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