let p1, p2, q1, q2, q3 be Point of (TOP-REAL 2); ( p1 <> p2 & LE q1,q2,p1,p2 & LE q2,q3,p1,p2 implies LE q1,q3,p1,p2 )
assume that
A1:
p1 <> p2
and
A2:
LE q1,q2,p1,p2
and
A3:
LE q2,q3,p1,p2
; LE q1,q3,p1,p2
A4:
q1 in LSeg (p1,p2)
by A2;
A5:
q2 in LSeg (p1,p2)
by A2;
A6:
q3 in LSeg (p1,p2)
by A3;
consider s1 being Real such that
A7:
q1 = ((1 - s1) * p1) + (s1 * p2)
and
0 <= s1
and
A8:
s1 <= 1
by A4;
consider s2 being Real such that
A9:
q2 = ((1 - s2) * p1) + (s2 * p2)
and
A10:
0 <= s2
and
A11:
s2 <= 1
by A5;
A12:
s1 <= s2
by A2, A7, A8, A9, A10, A11;
consider s3 being Real such that
A13:
q3 = ((1 - s3) * p1) + (s3 * p2)
and
A14:
0 <= s3
and
A15:
s3 <= 1
by A6;
s2 <= s3
by A3, A9, A11, A13, A14, A15;
then A16:
s1 <= s3
by A12, XXREAL_0:2;
thus
LE q1,q3,p1,p2
verumproof
thus
(
q1 in LSeg (
p1,
p2) &
q3 in LSeg (
p1,
p2) )
by A2, A3;
JORDAN3:def 5 for b1, b2 being object holds
( not 0 <= b1 or not b1 <= 1 or not q1 = ((1 - b1) * p1) + (b1 * p2) or not 0 <= b2 or not b2 <= 1 or not q3 = ((1 - b2) * p1) + (b2 * p2) or b1 <= b2 )
let r1,
r2 be
Real;
( not 0 <= r1 or not r1 <= 1 or not q1 = ((1 - r1) * p1) + (r1 * p2) or not 0 <= r2 or not r2 <= 1 or not q3 = ((1 - r2) * p1) + (r2 * p2) or r1 <= r2 )
assume that
0 <= r1
and
r1 <= 1
and A17:
q1 = ((1 - r1) * p1) + (r1 * p2)
and
0 <= r2
and
r2 <= 1
and A18:
q3 = ((1 - r2) * p1) + (r2 * p2)
;
r1 <= r2
s1 = r1
by A1, A7, A17, JORDAN5A:2;
hence
r1 <= r2
by A1, A13, A16, A18, JORDAN5A:2;
verum
end;