:: Zermelo's Theorem
:: by Bogdan Nowak and S{\l}awomir Bia{\l}ecki
::
:: Received October 27, 1989
:: Copyright (c) 1990-2012 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 ) )
proofend;

theorem Th2: :: WELLSET1:2
for X, Y being set
for W being Relation st X <> {} &amp; Y <> {} &amp; W = [:X,Y:] holds
field W = X \/ Y
proofend;

scheme :: WELLSET1:sch 1
RSeparation{ F1() ->  set , P1[ Relation] } :
 ex B being set st
for R being Relation holds
( R in B iff ( R in F1() &amp; P1[R] ) )
proofend;

theorem Th3: :: WELLSET1:3
for x, y being set
for W being Relation st x in field W &amp; y in field W &amp; W is well-ordering &amp; not x in W -Seg y holds
[y,x] in W
proofend;

theorem Th4: :: WELLSET1:4
for x, y being set
for W being Relation st x in field W &amp; y in field W &amp; W is well-ordering &amp; x in W -Seg y holds
not [y,x] in W
proofend;

theorem Th5: :: WELLSET1:5
for F being Function
for D being set st ( for X being set st X in D holds
( not F . X in X &amp; F . X in union D ) ) holds
ex R being Relation st
( field R c= union D &amp; R is well-ordering &amp; not field R in D &amp; ( for y being set st y in field R holds
( R -Seg y in D &amp; F . (R -Seg y) = y ) ) )
proofend;

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 &amp; [x,y] in Z ) ) &amp; ( for y being set st y in M holds
ex x being set st
( x in X &amp; [x,y] in Z ) ) &amp; ( for x, z1, y, z2 being set st [x,z1] in Z &amp; [y,z2] in Z holds
( x = y iff z1 = z2 ) ) ) )
proofend;

theorem :: WELLSET1:6
for N being set ex R being Relation st
( R is well-ordering &amp; field R = N )
proofend;