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

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

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

assume
A <> B
; :: thesis: contradictionA4:
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 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

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