let A, B be Ordinal; :: thesis: ( A c= B iff aleph A c= aleph B )
A1: ( aleph A c< aleph B iff ( aleph A <> aleph B & aleph A c= aleph B ) ) ;
( A in B iff aleph A in aleph B ) by Th20;
hence ( A c= B iff aleph A c= aleph B ) by A1, Th21, ORDINAL1:11, XBOOLE_0:def 8; :: thesis: verum