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