let K, M, N be Cardinal; :: thesis: ( K +` M in K +` N implies M in N )
assume A1: ( K +` M in K +` N & not M in N ) ; :: thesis: contradiction
then ( N c= M & K c= K ) by CARD_1:14;
then K +` N c= K +` M by Th41;
hence contradiction by A1, CARD_1:14; :: thesis: verum