The abstract of the Mizar article:

Zermelo's Theorem

by

Bogdan Nowak, and

Slawomir Bialecki

Received October 27, 1989

MML identifier: WELLSET1

[ Mizar article, MML identifier index ]

environ

 vocabulary RELAT_1, FUNCT_1, BOOLE, WELLORD1, RELAT_2, TARSKI;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1,
      WELLORD1;
 constructors TARSKI, RELAT_2, WELLORD1, SUBSET_1, XBOOLE_0;
 clusters RELAT_1, FUNCT_1, SUBSET_1, ZFMISC_1, XBOOLE_0;
 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
 x in field R iff ex y st ([x,y] in R or [y,x] in R);

canceled;

theorem :: WELLSET1:3
 X <> {} & Y <> {} & W = [: X,Y :] implies field W = X \/ Y;

scheme R_Separation { A()-> set, P[Relation] } :
     ex B st for R being Relation holds R in B iff R in A() & P[R];

canceled 2;

theorem :: WELLSET1:6
  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:7
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:8
 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:9
   for N ex R st R is well-ordering & field R = N;