let X be set ; :: thesis: for A being Ordinal st X c= A holds

order_type_of (RelIncl X) c= A

let A be Ordinal; :: thesis: ( X c= A implies order_type_of (RelIncl X) c= A )

assume A1: X c= A ; :: thesis: order_type_of (RelIncl X) c= A

then A2: (RelIncl A) |_2 X = RelIncl X by Th1;

A3: RelIncl X is well-ordering by A1, Th2;

hence order_type_of (RelIncl X) c= A by A1, A4, A5, WELLORD1:53; :: thesis: verum

order_type_of (RelIncl X) c= A

let A be Ordinal; :: thesis: ( X c= A implies order_type_of (RelIncl X) c= A )

assume A1: X c= A ; :: thesis: order_type_of (RelIncl X) c= A

then A2: (RelIncl A) |_2 X = RelIncl X by Th1;

A3: RelIncl X is well-ordering by A1, Th2;

A4: now :: thesis: ( RelIncl A,(RelIncl A) |_2 X are_isomorphic implies order_type_of (RelIncl X) c= A )

assume
RelIncl A,(RelIncl A) |_2 X are_isomorphic
; :: thesis: order_type_of (RelIncl X) c= A

then RelIncl X, RelIncl A are_isomorphic by A2, WELLORD1:40;

hence order_type_of (RelIncl X) c= A by A3, Def2; :: thesis: verum

end;then RelIncl X, RelIncl A are_isomorphic by A2, WELLORD1:40;

hence order_type_of (RelIncl X) c= A by A3, Def2; :: thesis: verum

A5: now :: thesis: ( ex a being object st

( a in A & (RelIncl A) |_2 ((RelIncl A) -Seg a),(RelIncl A) |_2 X are_isomorphic ) implies order_type_of (RelIncl X) c= A )

field (RelIncl A) = A
by Def1;( a in A & (RelIncl A) |_2 ((RelIncl A) -Seg a),(RelIncl A) |_2 X are_isomorphic ) implies order_type_of (RelIncl X) c= A )

given a being object such that A6:
a in A
and

A7: (RelIncl A) |_2 ((RelIncl A) -Seg a),(RelIncl A) |_2 X are_isomorphic ; :: thesis: order_type_of (RelIncl X) c= A

reconsider a = a as Ordinal by A6;

A8: (RelIncl A) -Seg a = a by A6, Th3;

A9: a c= A by A6, ORDINAL1:def 2;

then (RelIncl A) |_2 a = RelIncl a by Th1;

then RelIncl X, RelIncl a are_isomorphic by A2, A7, A8, WELLORD1:40;

hence order_type_of (RelIncl X) c= A by A3, A9, Def2; :: thesis: verum

end;A7: (RelIncl A) |_2 ((RelIncl A) -Seg a),(RelIncl A) |_2 X are_isomorphic ; :: thesis: order_type_of (RelIncl X) c= A

reconsider a = a as Ordinal by A6;

A8: (RelIncl A) -Seg a = a by A6, Th3;

A9: a c= A by A6, ORDINAL1:def 2;

then (RelIncl A) |_2 a = RelIncl a by Th1;

then RelIncl X, RelIncl a are_isomorphic by A2, A7, A8, WELLORD1:40;

hence order_type_of (RelIncl X) c= A by A3, A9, Def2; :: thesis: verum

hence order_type_of (RelIncl X) c= A by A1, A4, A5, WELLORD1:53; :: thesis: verum