let n, m be Nat; :: thesis: ( ( n c= m implies n <= m ) & ( n <= m implies n c= m ) & ( n in m implies n < m ) & ( n < m implies n in m ) )
H: ( n = Segm n & m = Segm m ) ;

A: now :: thesis: ( n c= m implies n <= m )

assume n c= m ; :: thesis: n <= m
then card (Segm n) c= card (Segm m) ;
hence n <= m by NAT_1:40; :: thesis: verum

end;

now :: thesis: ( n <= m implies n c= m )

assume n <= m ; :: thesis: n c= m
then card (Segm n) c= card (Segm m) by NAT_1:40;
hence n c= m ; :: thesis: verum

end;

hence ( n c= m iff n <= m ) by A; :: thesis: ( n in m iff n < m )

A: now :: thesis: ( n in m implies n < m )

assume n in m ; :: thesis: n < m
then card n in card m ;
hence n < m by H, NAT_1:41; :: thesis: verum

end;

now :: thesis: ( n < m implies n in m )

assume n < m ; :: thesis: n in m
then card (Segm n) in card (Segm m) by NAT_1:41;
hence n in m ; :: thesis: verum

end;

hence ( n in m iff n < m ) by A; :: thesis: verum