begin
:: deftheorem Def1 defines RelIncl WELLORD2:def 1 :
for X being set
for b2 being Relation holds
( b2 = RelIncl X iff ( field b2 = X & ( for Y, Z being set st Y in X & Z in X holds
( [Y,Z] in b2 iff Y c= Z ) ) ) );
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
:: deftheorem Def2 defines order_type_of WELLORD2:def 2 :
for R being Relation st R is well-ordering holds
for b2 being Ordinal holds
( b2 = order_type_of R iff R, RelIncl b2 are_isomorphic );
:: deftheorem defines is_order_type_of WELLORD2:def 3 :
for A being Ordinal
for R being Relation holds
( A is_order_type_of R iff A = order_type_of R );
theorem
:: deftheorem defines are_equipotent WELLORD2:def 4 :
for X, Y being set holds
( X,Y are_equipotent iff ex f being Function st
( f is one-to-one & dom f = X & rng f = Y ) );
theorem
theorem Th25:
Lm1:
for X being set
for R being Relation st R is well-ordering & X, field R are_equipotent holds
ex R being Relation st R well_orders X
theorem Th26:
theorem
begin
theorem
theorem
theorem
theorem
theorem