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

theorem Th1: :: WELLSET1:1

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

proof end;

theorem Th2: :: WELLSET1:2

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 Th3: :: WELLSET1:3

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 Th4: :: WELLSET1:4

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

theorem :: WELLSET1:6

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

proof end;