let n be Nat; 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); ( 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)
; 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 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
not
p in LSeg (
p1,
q)
;
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;
verum 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; verum