let M, N be Cardinal; :: thesis: ( N is finite & not M is finite implies ( N in M & N c= M ) )
assume that
A1: N is finite and
A2: not M is finite ; :: thesis: ( N in M & N c= M )
A3: N in omega by A1, CARD_1:61;
omega c= M by A2, Th82;
hence N in M by A3; :: thesis: N c= M
thus N c= M by A1, A2; :: thesis: verum