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 ) ;

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;then card (Segm n) c= card (Segm m) ;

hence n <= m by NAT_1:40; :: thesis: verum

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

hence
( n c= m iff n <= m )
by A; :: thesis: ( n in m iff n < 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;then card (Segm n) c= card (Segm m) by NAT_1:40;

hence n c= m ; :: thesis: verum

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

hence
( n in m iff n < m )
by A; :: thesis: verumassume
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;then card (Segm n) in card (Segm m) by NAT_1:41;

hence n in m ; :: thesis: verum