let M be Cardinal; :: thesis: for a being Aleph st ( a c= M or a in M ) holds
( a +` M = M & M +` a = M & a *` M = M & M *` a = M )
let a be Aleph; :: thesis: ( ( a c= M or a in M ) implies ( a +` M = M & M +` a = M & a *` M = M & M *` a = M ) )
A1: card 0 in a by Th25;
assume A2: ( a c= M or a in M ) ; :: thesis: ( a +` M = M & M +` a = M & a *` M = M & M *` a = M )
then not M is finite by Th26;
hence ( a +` M = M & M +` a = M & a *` M = M & M *` a = M ) by A2, A1, CARD_2:76, CARD_4:16; :: thesis: verum