:: deftheorem defines LE JORDAN3:def 5 :
for p1, p2, q1, q2 being Point of (TOP-REAL 2) holds
( LE q1,q2,p1,p2 iff ( q1 in LSeg (p1,p2) & q2 in LSeg (p1,p2) & ( for r1, r2 being Real st 0 <= r1 & r1 <= 1 & q1 = ((1 - r1) * p1) + (r1 * p2) & 0 <= r2 & r2 <= 1 & q2 = ((1 - r2) * p1) + (r2 * p2) holds
r1 <= r2 ) ) );