let A, B be Ordinal; :: thesis: ( alef A = alef B implies A = B )
assume A1: alef A = alef B ; :: thesis: A = B

A2: now :: thesis: not B in A

assume B in A ; :: thesis: contradiction
then alef B in alef A by Th21;
hence contradiction by A1; :: thesis: verum

end;

now :: thesis: not A in B

assume A in B ; :: thesis: contradiction
then alef A in alef B by Th21;
hence contradiction by A1; :: thesis: verum

end;

hence A = B by A2, ORDINAL1:14; :: thesis: verum