let X, Y be finite set ; :: thesis: ( X c< Y implies ( card X < card Y & card X in card Y ) )
assume A1: X c< Y ; :: thesis: ( card X < card Y & card X in card Y )
then ( X c= Y & X <> Y ) by XBOOLE_0:def 8;
then A2: ( Y = X \/ (Y \ X) & X misses Y \ X & X is finite & Y \ X is finite ) by XBOOLE_1:45, XBOOLE_1:79;
then A3: card Y = (card X) + (card (Y \ X)) by Th53;

A4: now

assume card (Y \ X) = 0 ; :: thesis: contradiction
then Y \ X = {} ;
hence contradiction by A1, A2; :: thesis: verum

end;

A5: card X <= card Y by A3, NAT_1:11;
card X <> card Y by A3, A4;
hence card X < card Y by A5, XXREAL_0:1; :: thesis: card X in card Y
hence card X in card Y by NAT_1:45; :: thesis: verum