let K, M, N be Cardinal; :: thesis: ( K +` M in K +` N implies M in N )
assume that
A1: K +` M in K +` N and
A2: not M in N ; :: thesis: contradiction
N c= M by A2, CARD_1:4;
then K +` N c= K +` M by Th82;
hence contradiction by A1, CARD_1:4; :: thesis: verum