let M, N be Cardinal; :: thesis: ( M is finite & ( N c= M or N in M ) implies N is finite )
assume A1: ( M is finite & ( N c= M or N in M ) ) ; :: thesis: N is finite
then N c= M by CARD_1:13;
hence N is finite by A1; :: thesis: verum