:: Zermelo's Theorem :: by Bogdan Nowak and S{\l}awomir Bia{\l}ecki :: :: Received October 27, 1989 :: Copyright (c) 1990-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies RELAT_1, FUNCT_1, XBOOLE_0, ZFMISC_1, SUBSET_1, WELLORD1, RELAT_2, TARSKI; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1, WELLORD1; constructors TARSKI, SUBSET_1, RELAT_2, WELLORD1, XTUPLE_0; registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1; requirements SUBSET, BOOLE; begin reserve a,b,x,y,z,z1,z2,z3,y1,y3,y4,A,B,C,D,G,M,N,X,Y,Z,W0,W00 for set, R,S,T, W,W1,W2 for Relation, F,H,H1 for Function; theorem :: WELLSET1:1 for x being object holds x in field R iff ex y being object st ([x,y] in R or [y,x] in R); theorem :: WELLSET1:2 X <> {} & Y <> {} & W = [: X,Y :] implies field W = X \/ Y; scheme :: WELLSET1:sch 1 RSeparation { A()-> set, P[Relation] } : ex B st for R being Relation holds R in B iff R in A() & P[R]; theorem :: WELLSET1:3 for x,y,W st x in field W & y in field W & W is well-ordering holds not x in W-Seg(y) implies [y,x] in W; theorem :: WELLSET1:4 for x,y,W st x in field W & y in field W & W is well-ordering holds x in W-Seg(y) implies not [y,x] in W; theorem :: WELLSET1:5 for F,D st (for X st X in D holds not F.X in X & F.X in union D) ex R st field R c= union D & R is well-ordering & not field R in D & for y st y in field R holds R-Seg(y) in D & F.(R-Seg(y)) = y; theorem :: WELLSET1:6 for N ex R st R is well-ordering & field R = N;