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