let M be Cardinal; :: thesis: for a being Aleph st ( a c= M or a in M ) holds
M is Aleph
let a be Aleph; :: thesis: ( ( a c= M or a in M ) implies M is Aleph )
assume ( a c= M or a in M ) ; :: thesis: M is Aleph
then ( omega c= a & a c= M ) by Th25, CARD_1:13;
then omega c= M by XBOOLE_1:1;
hence M is Aleph by CARD_3:102; :: thesis: verum