theorem :: CARD_2:48

for X, Y being finite set st X c< Y holds
( card X < card Y & card X in Segm (card Y) )