theorem LM519B1: :: ORDEQ_02:9

for a, b, z being Real
for p, q, x being Point of (REAL-NS 1) st p = <*a*> & q = <*b*> & x = <*z*> holds
( ( z in ].a,b.[ implies x in ].p,q.[ ) & ( x in ].p,q.[ implies ( a <> b & ( a < b implies z in ].a,b.[ ) & ( a > b implies z in ].b,a.[ ) ) ) )