:: deftheorem defines LT JORDAN3:def 6 :
for p1, p2, q1, q2 being Point of (TOP-REAL 2) holds
( LT q1,q2,p1,p2 iff ( LE q1,q2,p1,p2 & q1 <> q2 ) );