for x, y, z being Nat holds
( x in (Segm y) \ (Segm z) iff ( z <= x & x < y ) )