theorem LM519D: :: ORDEQ_02:11

for a, b being Real
for p, q being Point of (REAL-NS 1)
for I being Function of REAL,(REAL-NS 1) st p = <*a*> & q = <*b*> & I = (proj (1,1)) " holds
( ( a <= b implies I .: [.a,b.] = [.p,q.] ) & ( a < b implies I .: ].a,b.[ = ].p,q.[ ) )