theorem LM519C1: :: ORDEQ_02:10

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 implies z in [.a,b.] ) & ( a >= b implies z in [.b,a.] ) ) ) )