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