let A, B be Ordinal; :: thesis: ( A c= B iff alef A c= alef B )
( ( A c< B implies ( A <> B & A c= B ) ) & ( A <> B & A c= B implies A c< B ) & ( alef A c< alef B implies ( alef A <> alef B & alef A c= alef B ) ) & ( alef A <> alef B & alef A c= alef B implies alef A c< alef B ) ) by XBOOLE_0:def 8;
then ( ( A in B implies alef A in alef B ) & ( alef A in alef B implies A in B ) & ( alef A = alef B implies A = B ) & ( not alef A c= alef B or alef A = alef B or alef A in alef B ) & ( ( alef A = alef B or alef A in alef B ) implies alef A c= alef B ) & ( not A c= B or A = B or A in B ) & ( ( A = B or A in B ) implies A c= B ) ) by Th41, Th42, ORDINAL1:21, ORDINAL1:def 2;
hence ( A c= B iff alef A c= alef B ) ; :: thesis: verum