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 X is well-ordering by Th9;
A3: RelIncl A is well-ordering by Th7;
A4: field (RelIncl A) = A by Def1;
A5: (RelIncl A) |_2 X = RelIncl X by A1, Th8;

A6: 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 A5, WELLORD1:50;
hence order_type_of (RelIncl X) c= A by A2, Def2; :: thesis: verum

end;

now

given a being set such that A7: ( a in A & (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 A7;
A8: (RelIncl A) -Seg a = a by A7, Th10;
A9: a c= A by A7, ORDINAL1:def 2;
then (RelIncl A) |_2 a = RelIncl a by Th8;
then RelIncl X, RelIncl a are_isomorphic by A5, A7, A8, WELLORD1:50;
hence order_type_of (RelIncl X) c= A by A2, A9, Def2; :: thesis: verum

end;

hence order_type_of (RelIncl X) c= A by A1, A3, A4, A6, WELLORD1:64; :: thesis: verum