:: WELLSET1 semantic presentation

theorem Th1: :: WELLSET1:1
for b1 being set
for b2 being Relation holds
( b1 in field b2 iff ex b3 being set st
( [b1,b3] in b2 or [b3,b1] in b2 ) )
proof end;

theorem Th2: :: WELLSET1:2
canceled;

theorem Th3: :: WELLSET1:3
for b1, b2 being set
for b3 being Relation st b1 <> {} & b2 <> {} & b3 = [:b1,b2:] holds
field b3 = b1 \/ b2
proof end;

scheme :: WELLSET1:sch 1
s1{ F1() -> set , P1[ Relation] } :
ex b1 being set st
for b2 being Relation holds
( b2 in b1 iff ( b2 in F1() & P1[b2] ) )
proof end;

theorem Th4: :: WELLSET1:4
canceled;

theorem Th5: :: WELLSET1:5
canceled;

theorem Th6: :: WELLSET1:6
for b1, b2 being set
for b3 being Relation st b1 in field b3 & b2 in field b3 & b3 is well-ordering & not b1 in b3 -Seg b2 holds
[b2,b1] in b3
proof end;

theorem Th7: :: WELLSET1:7
for b1, b2 being set
for b3 being Relation st b1 in field b3 & b2 in field b3 & b3 is well-ordering & b1 in b3 -Seg b2 holds
not [b2,b1] in b3
proof end;

theorem Th8: :: WELLSET1:8
for b1 being Function
for b2 being set st ( for b3 being set st b3 in b2 holds
( not b1 . b3 in b3 & b1 . b3 in union b2 ) ) holds
ex b3 being Relation st
( field b3 c= union b2 & b3 is well-ordering & not field b3 in b2 & ( for b4 being set st b4 in field b3 holds
( b3 -Seg b4 in b2 & b1 . (b3 -Seg b4) = b4 ) ) )
proof end;

Lemma6: for b1, b2 being set holds
( b1,b2 are_equipotent iff ex b3 being set st
( ( for b4 being set st b4 in b1 holds
ex b5 being set st
( b5 in b2 & [b4,b5] in b3 ) ) & ( for b4 being set st b4 in b2 holds
ex b5 being set st
( b5 in b1 & [b5,b4] in b3 ) ) & ( for b4, b5, b6, b7 being set st [b4,b5] in b3 & [b6,b7] in b3 holds
( b4 = b6 iff b5 = b7 ) ) ) )
proof end;

theorem Th9: :: WELLSET1:9
for b1 being set ex b2 being Relation st
( b2 is well-ordering & field b2 = b1 )
proof end;