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 :: thesis: not A in B

A4: field (RelIncl B) = B by Def1;
assume A5: A in B ; :: thesis: contradiction
then A = (RelIncl B) -Seg A by Th3;
then RelIncl A = (RelIncl B) |_2 ((RelIncl B) -Seg A) by A4, Th1, WELLORD1:9;
hence contradiction by A2, A5, A4, WELLORD1:40, WELLORD1:46; :: thesis: verum

end;

assume A <> B ; :: thesis: contradiction
then A6: ( A in B or B in A ) by ORDINAL1:14;
then B = (RelIncl A) -Seg B by A3, Th3;
then RelIncl B = (RelIncl A) |_2 ((RelIncl A) -Seg B) by A1, Th1, WELLORD1:9;
hence contradiction by A2, A6, A3, A1, WELLORD1:46; :: thesis: verum