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

A2: now

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

end;

now

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

end;

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