let m, n be Nat; :: thesis: ( card (Segm n) in card (Segm m) iff n < m )
( card (Segm n) c< card (Segm m) iff ( card (Segm n) c= card (Segm m) & card (Segm n) <> card (Segm m) ) ) ;
hence ( card (Segm n) in card (Segm m) iff n < m ) by Th27, ORDINAL1:11, ORDINAL1:def 2; :: thesis: verum