let n be Nat; :: thesis: for p1, p2, q1, q2 being Point of (TOP-REAL n) st q1 in LSeg p1,p2 & q2 in LSeg p1,p2 holds
LSeg q1,q2 c= LSeg p1,p2
let p1, p2, q1, q2 be Point of (TOP-REAL n); :: thesis: ( q1 in LSeg p1,p2 & q2 in LSeg p1,p2 implies LSeg q1,q2 c= LSeg p1,p2 )
assume that
A1: q1 in LSeg p1,p2 and
A2: q2 in LSeg p1,p2 ; :: thesis: LSeg q1,q2 c= LSeg p1,p2
A3: LSeg p1,p2 = (LSeg p1,q1) \/ (LSeg q1,p2) by A1, Th11;

now

per cases ( q2 in LSeg p1,q1 or q2 in LSeg q1,p2 ) by A2, A3, XBOOLE_0:def 3;

suppose A4: q2 in LSeg p1,q1 ; :: thesis: LSeg q1,q2 c= LSeg p1,p2

A5: LSeg p1,q1 c= LSeg p1,p2 by A1, Lm1;
LSeg q2,q1 c= LSeg p1,q1 by A4, Lm1;
hence LSeg q1,q2 c= LSeg p1,p2 by A5, XBOOLE_1:1; :: thesis: verum

end;

suppose A6: q2 in LSeg q1,p2 ; :: thesis: LSeg q1,q2 c= LSeg p1,p2

A7: LSeg q1,p2 c= LSeg p1,p2 by A1, Lm1;
LSeg q1,q2 c= LSeg q1,p2 by A6, Lm1;
hence LSeg q1,q2 c= LSeg p1,p2 by A7, XBOOLE_1:1; :: thesis: verum

end;

end;

end;

hence LSeg q1,q2 c= LSeg p1,p2 ; :: thesis: verum