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;

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;

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 )

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;

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