Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989
Association of Mizar Users
Warsaw University, Bialystok
Supported by RPBP.III-24.C1.
We prove basic facts about enumerated sets:
definitional theorems and their immediate consequences, some theorems related to
the decomposition of an enumerated set into union of two sets, facts about
removing elements that occur more than once,
and facts about permutations of enumerated sets (with the length $\le$ 4).
The article includes also schemes enabling instantiation of up to nine universal
The terminology and notation used in this paper have been
introduced in the following articles
Contents (PDF format)
Tarski Grothendieck set theory.
Journal of Formalized Mathematics,
Received January 8, 1989
Download a postscript version,
MML identifier index,
Mizar home page]