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 A1: ( p in LSeg p1,p2 & q in LSeg p1,p2 ) ; :: thesis: LSeg p1,p2 = ((LSeg p1,p) \/ (LSeg p,q)) \/ (LSeg q,p2)
( p1 in LSeg p1,p2 & p2 in LSeg p1,p2 ) by Th6;
then ( LSeg p1,p c= LSeg p1,p2 & LSeg p,q c= LSeg p1,p2 & LSeg q,p2 c= LSeg p1,p2 ) by A1, Th12;
then ( (LSeg p1,p) \/ (LSeg p,q) c= LSeg p1,p2 & LSeg q,p2 c= LSeg p1,p2 ) by XBOOLE_1:8;
then A2: ((LSeg p1,p) \/ (LSeg p,q)) \/ (LSeg q,p2) c= LSeg p1,p2 by XBOOLE_1:8;
A3: LSeg p1,p2 = (LSeg p1,q) \/ (LSeg q,p2) by A1, Th11;

now

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 A3, Th11; :: 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, A3, XBOOLE_0:def 3;
then A4: LSeg q,p2 = (LSeg q,p) \/ (LSeg p,p2) by Th11;
LSeg p1,p2 = (LSeg p1,p) \/ (LSeg p,p2) by A1, Th11;
then A5: LSeg p1,p2 c= (LSeg p1,p) \/ (LSeg q,p2) by A4, XBOOLE_1:7, XBOOLE_1:9;
A6: (LSeg p1,p) \/ (LSeg q,p2) c= ((LSeg p1,p) \/ (LSeg q,p2)) \/ (LSeg p,q) by XBOOLE_1:7;
((LSeg p1,p) \/ (LSeg q,p2)) \/ (LSeg p,q) = ((LSeg p1,p) \/ (LSeg p,q)) \/ (LSeg q,p2) by XBOOLE_1:4;
hence LSeg p1,p2 c= ((LSeg p1,p) \/ (LSeg p,q)) \/ (LSeg q,p2) by A5, A6, XBOOLE_1:1; :: thesis: verum

end;

end;

end;

hence LSeg p1,p2 = ((LSeg p1,p) \/ (LSeg p,q)) \/ (LSeg q,p2) by A2, XBOOLE_0:def 10; :: thesis: verum