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 Th89;
hence contradiction by A1, CARD_1:4; :: thesis: verum