let A, B be Ordinal; :: thesis: ( aleph A = aleph B implies A = B )
assume A1: aleph A = aleph B ; :: thesis: A = B
A2: now :: thesis: not B in A
assume B in A ; :: thesis: contradiction
then aleph B in aleph A by Th20;
hence contradiction by A1; :: thesis: verum
end;
now :: thesis: not A in B
assume A in B ; :: thesis: contradiction
then aleph A in aleph B by Th20;
hence contradiction by A1; :: thesis: verum
end;
hence A = B by A2, ORDINAL1:14; :: thesis: verum