:: by Bogdan Nowak and S{\l}awomir Bia{\l}ecki

::

:: Received October 27, 1989

:: Copyright (c) 1990-2019 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 ) )

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

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

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 ) ) )

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;