:: 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{ F1() -> set , P1[ Relation] } :
ex B being set st
for R being Relation holds
( R in B iff ( R in F1() & P1[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;