theorem Th2: :: MYCIELSK:2

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