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, Th12;
A4: LSeg p1,p2 = (LSeg p1,q) \/ (LSeg q,p2) by A2, Th11;

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

end;

end;

end;

p1 in LSeg p1,p2 by RLTOPSP1:69;
then LSeg p1,p c= LSeg p1,p2 by A1, Th12;
then A9: (LSeg p1,p) \/ (LSeg p,q) c= LSeg p1,p2 by A3, XBOOLE_1:8;
p2 in LSeg p1,p2 by RLTOPSP1:69;
then LSeg q,p2 c= LSeg p1,p2 by A2, Th12;
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, XBOOLE_0:def 10; :: thesis: verum