let M, N be Cardinal; :: thesis: ( not M is finite & ( N c= M or N in M ) implies ( M *` N c= M & N *` M c= M ) )
assume ( not M is finite & ( N c= M or N in M ) ) ; :: thesis: ( M *` N c= M & N *` M c= M )
then ( M *` N = M or not 0 in N ) by Th16;
then ( M *` N c= M or ( N = 0 & M *` 0 = 0 & 0 c= M ) ) by CARD_2:20, ORDINAL3:8;
hence ( M *` N c= M & N *` M c= M ) ; :: thesis: verum