let A, B be Ordinal; :: thesis: ( A c= B iff alef A c= alef B )
A1: ( A c< B iff ( A <> B & A c= B ) ) by XBOOLE_0:def 8;
A2: ( alef A c< alef B iff ( alef A <> alef B & alef A c= alef B ) ) by XBOOLE_0:def 8;
( A in B iff alef A in alef B ) by Th41;
hence ( A c= B iff alef A c= alef B ) by A1, A2, Th42, ORDINAL1:11, ORDINAL1:def 2; :: thesis: verum