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, Th5;
now :: thesis: LSeg (q1,q2) c= LSeg (p1,p2)
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; :: 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; :: thesis: verum
end;
end;
end;
hence LSeg (q1,q2) c= LSeg (p1,p2) ; :: thesis: verum