let n be Element of NAT ; :: thesis:
let p1, p2 be Point of (TOP-REAL n); :: thesis:
let P be Subset of (TOP-REAL n); :: thesis:
assume A1: ( P c= LSeg p1,p2 & p1 in P & p2 in P & P is connected ) ; :: thesis:
then reconsider L = LSeg p1,p2 as non empty Subset of (TOP-REAL n) ;

now

assume not LSeg p1,p2 c= P ; :: thesis:
then consider x0 being set such that
A2: ( x0 in LSeg p1,p2 & not x0 in P ) by TARSKI:def 3;
reconsider p0 = x0 as Point of (TOP-REAL n) by A2;
A3: p1 in LSeg p1,p2 by RLTOPSP1:69;
then A4: LSeg p1,p0 c= L by A2, TOPREAL1:12;
A5: (LSeg p1,p0) \ {p0} c= LSeg p1,p0 by XBOOLE_1:36;
A6: the carrier of ((TOP-REAL n) | L) = [#] ((TOP-REAL n) | L)
.= L by PRE_TOPC:def 10 ;
then reconsider R1 = (LSeg p1,p0) \ {p0} as Subset of ((TOP-REAL n) | L) by A4, A5, XBOOLE_1:1;
A7: p2 in LSeg p1,p2 by RLTOPSP1:69;
then A8: LSeg p0,p2 c= L by A2, TOPREAL1:12;
(LSeg p0,p2) \ {p0} c= LSeg p0,p2 by XBOOLE_1:36;
then reconsider R2 = (LSeg p0,p2) \ {p0} as Subset of ((TOP-REAL n) | L) by A6, A8, XBOOLE_1:1;
reconsider PX = P as Subset of ((TOP-REAL n) | L) by A1, A6;
reconsider PX1 = LSeg p1,p0 as Subset of ((TOP-REAL n) | L) by A2, A3, A6, TOPREAL1:12;
reconsider PX2 = LSeg p0,p2 as Subset of ((TOP-REAL n) | L) by A2, A6, A7, TOPREAL1:12;
A9: (TOP-REAL n) | L is T_2 by TOPMETR:3;
LSeg p1,p0 is compact by SPPOL_1:28;
then PX1 is compact by COMPTS_1:28;
then PX1 is closed by A9, COMPTS_1:16;
then A10: Cl PX1 = PX1 by PRE_TOPC:52;
A11: PX is connected by A1, JORDAN2C:15;
A12: R2 c= PX2 by XBOOLE_1:36;
A13: R1 c= PX1 by XBOOLE_1:36;
A14: Cl R1 c= Cl PX1 by PRE_TOPC:49, XBOOLE_1:36;
A15: PX1 /\ PX2 = {p0} by A2, TOPREAL1:14;
PX1 /\ R2 = (PX1 /\ PX2) \ {p0} by XBOOLE_1:49
.= {} by A15, XBOOLE_1:37 ;
then (Cl R1) /\ R2 = {} by A10, A14, XBOOLE_1:3, XBOOLE_1:27;
then A16: Cl R1 misses R2 by XBOOLE_0:def 7;
LSeg p0,p2 is compact by SPPOL_1:28;
then PX2 is compact by COMPTS_1:28;
then PX2 is closed by A9, COMPTS_1:16;
then A17: Cl PX2 = PX2 by PRE_TOPC:52;
A18: Cl R2 c= Cl PX2 by PRE_TOPC:49, XBOOLE_1:36;
A19: PX1 /\ PX2 = {p0} by A2, TOPREAL1:14;
R1 /\ PX2 = (PX1 /\ PX2) \ {p0} by XBOOLE_1:49
.= {} by A19, XBOOLE_1:37 ;
then R1 /\ (Cl R2) = {} by A17, A18, XBOOLE_1:3, XBOOLE_1:27;
then R1 misses Cl R2 by XBOOLE_0:def 7;
then A20: R1,R2 are_separated by A16, CONNSP_1:def 1;
A21: {p0} c= LSeg p1,p0

proof

let d be set ; :: according to TARSKI:def 3 :: thesis:
assume d in {p0} ; :: thesis:
then d = p0 by TARSKI:def 1;
hence d in LSeg p1,p0 by RLTOPSP1:69; :: thesis:

end;

A22: {p0} c= LSeg p0,p2

proof

let d be set ; :: according to TARSKI:def 3 :: thesis:
assume d in {p0} ; :: thesis:
then d = p0 by TARSKI:def 1;
hence d in LSeg p0,p2 by RLTOPSP1:69; :: thesis:

end;

A23: L = (LSeg p1,p0) \/ (LSeg p0,p2) by A2, TOPREAL1:11
.= (((LSeg p1,p0) \ {p0}) \/ {p0}) \/ (LSeg p0,p2) by A21, XBOOLE_1:45
.= ((LSeg p1,p0) \ {p0}) \/ ({p0} \/ (LSeg p0,p2)) by XBOOLE_1:4
.= R1 \/ PX2 by A22, XBOOLE_1:12
.= R1 \/ ((PX2 \ {p0}) \/ {p0}) by A22, XBOOLE_1:45
.= (R1 \/ {p0}) \/ R2 by XBOOLE_1:4 ;
A24: P c= R1 \/ R2

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume A25: z in P ; :: thesis:
then ( z in R1 \/ {p0} or z in R2 ) by A1, A23, XBOOLE_0:def 3;
then ( z in R1 or z in {p0} or z in R2 ) by XBOOLE_0:def 3;
hence z in R1 \/ R2 by A2, A25, TARSKI:def 1, XBOOLE_0:def 3; :: thesis:

end;

A26: now

assume P c= R1 ; :: thesis:
then A27: p2 in R1 by A1;
p2 in PX2 by RLTOPSP1:69;
then p2 in PX1 /\ PX2 by A13, A27, XBOOLE_0:def 4;
hence contradiction by A1, A2, A19, TARSKI:def 1; :: thesis:

end;

now

assume P c= R2 ; :: thesis:
then A28: p1 in R2 by A1;
p1 in PX1 by RLTOPSP1:69;
then p1 in PX1 /\ PX2 by A12, A28, XBOOLE_0:def 4;
hence contradiction by A1, A2, A19, TARSKI:def 1; :: thesis:

end;

hence contradiction by A11, A20, A24, A26, CONNSP_1:17; :: thesis:

end;

hence P = LSeg p1,p2 by A1, XBOOLE_0:def 10; :: thesis: