Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

### Zermelo's Theorem

by
Bogdan Nowak, and
Slawomir Bialecki

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;
```