let X, Y be finite set ; :: thesis: ( X c< Y implies ( card X < card Y & card X in Segm (card Y) ) )
assume A1: X c< Y ; :: thesis: ( card X < card Y & card X in Segm (card Y) )
then X c= Y ;
then A2: Y = X \/ (Y \ X) by XBOOLE_1:45;
then A3: card Y = (card X) + (card (Y \ X)) by Th39, XBOOLE_1:79;
then A4: card X <= card Y by NAT_1:11;
now :: thesis: not card (Y \ X) = 0
assume card (Y \ X) = 0 ; :: thesis: contradiction
then Y \ X = {} ;
hence contradiction by A1, A2; :: thesis: verum
end;
then card X <> card Y by A3;
hence card X < card Y by A4, XXREAL_0:1; :: thesis: card X in Segm (card Y)
hence card X in Segm (card Y) by NAT_1:44; :: thesis: verum