let A, B be Ordinal; :: thesis: ( RelIncl A, RelIncl B are_isomorphic implies A = B )
A1: field (RelIncl A) = A by Def1;
assume A2: RelIncl A, RelIncl B are_isomorphic ; :: thesis: A = B

A3: now

A4: RelIncl B is well-ordering by Th7;
A5: field (RelIncl B) = B by Def1;
assume A6: A in B ; :: thesis: contradiction
then A = (RelIncl B) -Seg A by Th10;
then RelIncl A = (RelIncl B) |_2 ((RelIncl B) -Seg A) by A5, Th8, WELLORD1:13;
hence contradiction by A2, A6, A5, A4, WELLORD1:50, WELLORD1:57; :: thesis: verum

end;

assume A <> B ; :: thesis: contradiction
then A7: ( A in B or B in A ) by ORDINAL1:24;
then B = (RelIncl A) -Seg B by A3, Th10;
then RelIncl B = (RelIncl A) |_2 ((RelIncl A) -Seg B) by A1, Th8, WELLORD1:13;
hence contradiction by A2, A7, A3, A1, Th7, WELLORD1:57; :: thesis: verum