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