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 Th8;
A3: RelIncl X is well-ordering by A1, Th9;

A4: now

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

given a being set 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, Th10;
A9: a c= A by A6, ORDINAL1:def 2;
then (RelIncl A) |_2 a = RelIncl a by Th8;
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, Th7, WELLORD1:53; :: thesis: verum