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 ) )
card 0 in a by Th15;
then A1: 0 in a ;
assume A2: ( a c= M or a in M ) ; :: thesis: ( a +` M = M & M +` a = M & a *` M = M & M *` a = M )
then A3: M is infinite by Th16;
A4: a c= M by A2, ORDINAL1:16;
thus a +` M = M by CARD_2:76, A3, A4; :: thesis: ( M +` a = M & a *` M = M & M *` a = M )
thus M +` a = M by CARD_2:76, A3, A4; :: thesis: ( a *` M = M & M *` a = M )
thus a *` M = M by A1, CARD_4:16, A3, A4; :: thesis: M *` a = M
thus M *` a = M by A1, CARD_4:16, A3, A4; :: thesis: verum