for m, n being Nat holds
( card (Segm n) c= card (Segm m) iff n <= m ) by Th27;