let x, y, z be Nat; :: thesis: ( x in (Segm y) \ (Segm z) iff ( z <= x & x < y ) )

hereby :: thesis: ( z <= x & x < y implies x in (Segm y) \ (Segm z) )

assume A1: x in (Segm y) \ (Segm z) ; :: thesis: ( z <= x & x < y )
not x in Segm z by A1, XBOOLE_0:def 5;
hence z <= x by NAT_1:44; :: thesis: x < y
x in Segm y by A1, XBOOLE_0:def 5;
hence x < y by NAT_1:44; :: thesis: verum

end;

assume ( z <= x & x < y ) ; :: thesis: x in (Segm y) \ (Segm z)
then ( x in Segm y & not x in Segm z ) by NAT_1:44;
hence x in (Segm y) \ (Segm z) by XBOOLE_0:def 5; :: thesis: verum