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

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

assume A: x in y \ z ; :: thesis: ( z <= x & x < y )
not x in z by A, XBOOLE_0:def 5;
hence z <= x by NAT_1:45; :: thesis: x < y
thus x < y by A, NAT_1:45; :: thesis: verum

end;

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