let X be set ; :: thesis:
let A be Ordinal; :: thesis:
assume A1: X c= A ; :: thesis:
then A2: (RelIncl A) |_2 X = RelIncl X by Th1;
A3: RelIncl X is well-ordering by A1, Th2;

A4: now :: thesis:

assume RelIncl A,(RelIncl A) |_2 X are_isomorphic ; :: thesis:
then RelIncl X, RelIncl A are_isomorphic by A2, WELLORD1:40;
hence order_type_of (RelIncl X) c= A by A3, Def2; :: thesis:

end;

A5: now :: thesis:

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:
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:

end;

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