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 that
A1: P c= LSeg p1,p2 and
A2: p1 in P and
A3: p2 in P and
A4: P is connected ; :: thesis:
reconsider L = LSeg p1,p2 as non empty Subset of (TOP-REAL n) by A1, A2;

now

A5: the carrier of ((TOP-REAL n) | L) = [#] ((TOP-REAL n) | L)
.= L by PRE_TOPC:def 10 ;
then reconsider PX = P as Subset of ((TOP-REAL n) | L) by A1;
assume not LSeg p1,p2 c= P ; :: thesis:
then consider x0 being set such that
A6: x0 in LSeg p1,p2 and
A7: not x0 in P by TARSKI:def 3;
reconsider p0 = x0 as Point of (TOP-REAL n) by A6;
A8: (LSeg p0,p2) \ {p0} c= LSeg p0,p2 by XBOOLE_1:36;
A9: p1 in LSeg p1,p2 by RLTOPSP1:69;
then reconsider PX1 = LSeg p1,p0 as Subset of ((TOP-REAL n) | L) by A6, A5, TOPREAL1:12;
A10: (LSeg p1,p0) \ {p0} c= LSeg p1,p0 by XBOOLE_1:36;
LSeg p1,p0 c= L by A6, A9, TOPREAL1:12;
then reconsider R1 = (LSeg p1,p0) \ {p0} as Subset of ((TOP-REAL n) | L) by A10, A5, XBOOLE_1:1;
A11: (TOP-REAL n) | L is T_2 by TOPMETR:3;
A12: p2 in LSeg p1,p2 by RLTOPSP1:69;
then LSeg p0,p2 c= L by A6, TOPREAL1:12;
then reconsider R2 = (LSeg p0,p2) \ {p0} as Subset of ((TOP-REAL n) | L) by A5, A8, XBOOLE_1:1;
reconsider PX2 = LSeg p0,p2 as Subset of ((TOP-REAL n) | L) by A6, A5, A12, TOPREAL1:12;
A13: PX1 /\ PX2 = {p0} by A6, TOPREAL1:14;
A14: R1 c= PX1 by XBOOLE_1:36;

A15: now

assume P c= R1 ; :: thesis:
then A16: p2 in R1 by A3;
p2 in PX2 by RLTOPSP1:69;
then p2 in PX1 /\ PX2 by A14, A16, XBOOLE_0:def 4;
hence contradiction by A3, A7, A13, TARSKI:def 1; :: thesis:

end;

A17: {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;

A18: {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;

LSeg p0,p2 is compact ;
then PX2 is compact by COMPTS_1:28;
then PX2 is closed by A11, COMPTS_1:16;
then A19: Cl PX2 = PX2 by PRE_TOPC:52;
A20: Cl R2 c= Cl PX2 by PRE_TOPC:49, XBOOLE_1:36;
R1 /\ PX2 = (PX1 /\ PX2) \ {p0} by XBOOLE_1:49
.= {} by A13, XBOOLE_1:37 ;
then R1 /\ (Cl R2) = {} by A19, A20, XBOOLE_1:3, XBOOLE_1:27;
then A21: R1 misses Cl R2 by XBOOLE_0:def 7;
A22: PX1 /\ PX2 = {p0} by A6, TOPREAL1:14;
A23: R2 c= PX2 by XBOOLE_1:36;

A24: now

assume P c= R2 ; :: thesis:
then A25: p1 in R2 by A2;
p1 in PX1 by RLTOPSP1:69;
then p1 in PX1 /\ PX2 by A23, A25, XBOOLE_0:def 4;
hence contradiction by A2, A7, A13, TARSKI:def 1; :: thesis:

end;

LSeg p1,p0 is compact ;
then PX1 is compact by COMPTS_1:28;
then PX1 is closed by A11, COMPTS_1:16;
then A26: Cl PX1 = PX1 by PRE_TOPC:52;
A27: L = (LSeg p1,p0) \/ (LSeg p0,p2) by A6, TOPREAL1:11
.= (((LSeg p1,p0) \ {p0}) \/ {p0}) \/ (LSeg p0,p2) by A17, XBOOLE_1:45
.= ((LSeg p1,p0) \ {p0}) \/ ({p0} \/ (LSeg p0,p2)) by XBOOLE_1:4
.= R1 \/ PX2 by A18, XBOOLE_1:12
.= R1 \/ ((PX2 \ {p0}) \/ {p0}) by A18, XBOOLE_1:45
.= (R1 \/ {p0}) \/ R2 by XBOOLE_1:4 ;
A28: P c= R1 \/ R2

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume A29: z in P ; :: thesis:
then ( z in R1 \/ {p0} or z in R2 ) by A1, A27, 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 A7, A29, TARSKI:def 1, XBOOLE_0:def 3; :: thesis:

end;

A30: Cl R1 c= Cl PX1 by PRE_TOPC:49, XBOOLE_1:36;
PX1 /\ R2 = (PX1 /\ PX2) \ {p0} by XBOOLE_1:49
.= {} by A22, XBOOLE_1:37 ;
then (Cl R1) /\ R2 = {} by A26, A30, XBOOLE_1:3, XBOOLE_1:27;
then Cl R1 misses R2 by XBOOLE_0:def 7;
then A31: R1,R2 are_separated by A21, CONNSP_1:def 1;
PX is connected by A4, JORDAN2C:15;
hence contradiction by A31, A28, A15, A24, CONNSP_1:17; :: thesis:

end;

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