The Library Committee decided to collect definitions and theorems from the Mizar Mathematical Library concerning boolean properties of sets into new articles. It is the first step in building Encyclopaedia of Mathematics in Mizar (EMM for short).
The first letter of EMM articles will be 'X' so any other article submitted to the MML with MML Identifier beginning with 'X' will not be accepted. These two new articles (authored by Library Committee) with MML identifiers XBOOLE_0 and XBOOLE_1 are built mainly on Mizar article Boolean Properties of Sets by Zinaida Trybulec and Halina Swieczkowska (MML Id: BOOLE).
XBOOLE_0 consists of basic definitions of the empty set, basic boolean operations (union, meet, difference and symmetric difference of two sets), attribute 'empty', predicates 'meets', 'misses', 'c<', 'are_c=-comparable' and redefinition of equality for sets, existential registrations of clusters for empty and non empty sets and functorial cluster that {} is empty and three schemes: Separation, Extensionality and SetEq.
XBOOLE_1 contains 'boolean' theorems collected from the MML with the help of MML Query. Any other 'boolean' (i.e. which use constructors from XBOOLE_0) theorem will be moved into XBOOLE series.
Note that requirement and vocabulary files have still identifiers BOOLE. What is especially important, the requirement that {} and arbitrary empty set are equal has been moved from requirement file SUBSET.
This revision had the big impact on the whole MML, references for theorems from BOOLE have to be replaced according to the attached list boolereplths.txt. Usually XBOOLE_0 has to be added as a 'notation', 'constructors', 'theorems' and 'schemes' directive. XBOOLE_1 can be safely added to 'theorems' directive.
Afterwards, we removed theorems which were straightforward consequences of another theorems (referenced by 'by'). Two articles (BOOLE and BVFUNC17) became void so we deleted them from the MML.
new BOOLE file added, contains proofs of four theorems which are obvious if the 'requirements BOOLE;' will be added to the environment declaration. BVFUNC16 became empty, so it was removed.
antisymmetry changed into asymmetry, (thanks to Piotr Rudnicki) this property occured only in HIDDEN, POLYNOM1, POLYNOM3).
SGRAPH1: SimpleGraphStruct is now descendant of 1-sorted (selector 'SVertices' has been changed into 'carrier').
JORDAN1J: revised by its author.
GRAPH1: the attribute 'Path-like' synonymous to 'one-to-one' was removed (with all occurences consequently replaced).
some irrelevant assumptions removed (AFVECT0, AFF_4, BVFUNC11, BVFUNC13, EUCLMETR, GROUP_4, JORDAN1, NAT_LAT, RLSUB_2, RLVECT_1).
MOD_1: completely reorganized; splitted conjunction theorems into single ones, removed corollaries from other articles, generalized theorems (mainly used facts from RLVECT_1, VECTSP_1). Similar revision in case of VECTSP_1.
WAYBEL_4: def 24 (pred x is_maximal_wrt X,R) was generalized to cover the case if x is not necessarily element of the carrier of some structure, now loci are at more general level. The same with dual def 26. DICKSON had to be revised slightly to use this feature.
XBOOLE_1: Theorems 14 and 20 (equivalences which were corollaries) became implicational now. Two new theorems were added, XBOOLE_1:84 and XBOOLE_1:90. References by XBOOLE_1 have to be increased by one or two (if greater than 84 and 88).
XBOOLE_0: added cluster stating that the set-theoretical union of non empty and arbitrary set is non empty (moved from AFPROJ).
INT_1: some theorems are now formulated for real numbers instead of integers.
REAL_2: number of theorems were formulated as conjunctions, some conjuncts were deleted as corollaries from other articles (mainly REAL_1). The description is in the file repl3233.txt. Note that replacement of references should not be done automatically without prompting the user.
corollaries were automatically removed (the detailed description is in the second part of the file).