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

A5: now :: thesis: LSeg (p1,p2) c= ((LSeg (p1,p)) \/ (LSeg (p,q))) \/ (LSeg (q,p2))

per cases ( p in LSeg (p1,q) or not p in LSeg (p1,q) ) ;

suppose p in LSeg (p1,q) ; :: thesis: LSeg (p1,p2) c= ((LSeg (p1,p)) \/ (LSeg (p,q))) \/ (LSeg (q,p2))

hence LSeg (p1,p2) c= ((LSeg (p1,p)) \/ (LSeg (p,q))) \/ (LSeg (q,p2)) by A4, Th5; :: thesis: verum

end;

suppose not p in LSeg (p1,q) ; :: thesis: LSeg (p1,p2) c= ((LSeg (p1,p)) \/ (LSeg (p,q))) \/ (LSeg (q,p2))

then p in LSeg (q,p2) by A1, A4, XBOOLE_0:def 3;
then A6: LSeg (q,p2) = (LSeg (q,p)) \/ (LSeg (p,p2)) by Th5;
LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) by A1, Th5;
then A7: LSeg (p1,p2) c= (LSeg (p1,p)) \/ (LSeg (q,p2)) by A6, XBOOLE_1:7, XBOOLE_1:9;
A8: ((LSeg (p1,p)) \/ (LSeg (q,p2))) \/ (LSeg (p,q)) = ((LSeg (p1,p)) \/ (LSeg (p,q))) \/ (LSeg (q,p2)) by XBOOLE_1:4;
(LSeg (p1,p)) \/ (LSeg (q,p2)) c= ((LSeg (p1,p)) \/ (LSeg (q,p2))) \/ (LSeg (p,q)) by XBOOLE_1:7;
hence LSeg (p1,p2) c= ((LSeg (p1,p)) \/ (LSeg (p,q))) \/ (LSeg (q,p2)) by A7, A8; :: thesis: verum

end;

end;

end;

p1 in LSeg (p1,p2) by RLTOPSP1:68;
then LSeg (p1,p) c= LSeg (p1,p2) by A1, Th6;
then A9: (LSeg (p1,p)) \/ (LSeg (p,q)) c= LSeg (p1,p2) by A3, XBOOLE_1:8;
p2 in LSeg (p1,p2) by RLTOPSP1:68;
then LSeg (q,p2) c= LSeg (p1,p2) by A2, Th6;
then ((LSeg (p1,p)) \/ (LSeg (p,q))) \/ (LSeg (q,p2)) c= LSeg (p1,p2) by A9, XBOOLE_1:8;
hence LSeg (p1,p2) = ((LSeg (p1,p)) \/ (LSeg (p,q))) \/ (LSeg (q,p2)) by A5; :: thesis: verum