let A, B be Ordinal; :: thesis: ( RelIncl A, RelIncl B are_isomorphic implies A = B )
assume A1: RelIncl A, RelIncl B are_isomorphic ; :: thesis: A = B
assume A <> B ; :: thesis: contradiction
then A2: ( A in B or B in A ) by ORDINAL1:24;

A3: now

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

end;

then A8: B = (RelIncl A) -Seg B by A2, Th10;
A9: field (RelIncl A) = A by Def1;
then RelIncl B = (RelIncl A) |_2 ((RelIncl A) -Seg B) by A8, Th8, WELLORD1:13;
hence contradiction by A1, A2, A3, A9, Th7, WELLORD1:57; :: thesis: verum