:: Zermelo's Theorem
:: by Bogdan Nowak and S{\l}awomir Bia{\l}ecki
::
:: Received October 27, 1989
:: Copyright (c) 1990-2011 Association of Mizar Users

begin

theorem Th1: :: WELLSET1:1

for x being set
for R being Relation holds
( x in field R iff ex y being set st
( [x,y] in R or [y,x] in R ) )

proof end;

theorem :: WELLSET1:2

canceled;

theorem Th3: :: WELLSET1:3

for X, Y being set
for W being Relation st X <> {} & Y <> {} & W = [:X,Y:] holds
field W = X \/ Y

proof end;

scheme :: WELLSET1:sch 1
RSeparation{ F₁() -> set , P₁[ Relation] } :

ex B being set st
for R being Relation holds
( R in B iff ( R in F₁() & P₁[R] ) )

proof end;

theorem :: WELLSET1:4

canceled;

theorem :: WELLSET1:5

canceled;

theorem Th6: :: WELLSET1:6

for x, y being set
for W being Relation st x in field W & y in field W & W is well-ordering & not x in W -Seg y holds
[y,x] in W

proof end;

theorem Th7: :: WELLSET1:7

for x, y being set
for W being Relation st x in field W & y in field W & W is well-ordering & x in W -Seg y holds
not [y,x] in W

proof end;

theorem Th8: :: WELLSET1:8

for F being Function
for D being set st ( for X being set st X in D holds
( not F . X in X & F . X in union D ) ) holds
ex R being Relation st
( field R c= union D & R is well-ordering & not field R in D & ( for y being set st y in field R holds
( R -Seg y in D & F . (R -Seg y) = y ) ) )

proof end;

Lm1: for X, M being set holds
( X,M are_equipotent iff ex Z being set st
( ( for x being set st x in X holds
ex y being set st
( y in M & [x,y] in Z ) ) & ( for y being set st y in M holds
ex x being set st
( x in X & [x,y] in Z ) ) & ( for x, z1, y, z2 being set st [x,z1] in Z & [y,z2] in Z holds
( x = y iff z1 = z2 ) ) ) )

proof end;

theorem :: WELLSET1:9

for N being set ex R being Relation st
( R is well-ordering & field R = N )

proof end;