let n be Nat; :: thesis: for p1, p2 being Point of (TOP-REAL n)
for P being Subset of (TOP-REAL n) st P c= LSeg (p1,p2) & p1 in P & p2 in P & P is connected holds
P = LSeg (p1,p2)
let p1, p2 be Point of (TOP-REAL n); :: thesis: for P being Subset of (TOP-REAL n) st P c= LSeg (p1,p2) & p1 in P & p2 in P & P is connected holds
P = LSeg (p1,p2)
let P be Subset of (TOP-REAL n); :: thesis: ( P c= LSeg (p1,p2) & p1 in P & p2 in P & P is connected implies P = LSeg (p1,p2) )
assume that
A1: P c= LSeg (p1,p2) and
A2: p1 in P and
A3: p2 in P and
A4: P is connected ; :: thesis: P = LSeg (p1,p2)
reconsider L = LSeg (p1,p2) as non empty Subset of (TOP-REAL n) by A1, A2;
now :: thesis: LSeg (p1,p2) c= P
A5: the carrier of ((TOP-REAL n) | L) = [#] ((TOP-REAL n) | L)
.= L by PRE_TOPC:def 5 ;
then reconsider PX = P as Subset of ((TOP-REAL n) | L) by A1;
assume not LSeg (p1,p2) c= P ; :: thesis: contradiction
then consider x0 being object such that
A6: x0 in LSeg (p1,p2) and
A7: not x0 in P ;
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:68;
then reconsider PX1 = LSeg (p1,p0) as Subset of ((TOP-REAL n) | L) by A6, A5, TOPREAL1:6;
A10: (LSeg (p1,p0)) \ {p0} c= LSeg (p1,p0) by XBOOLE_1:36;
LSeg (p1,p0) c= L by A6, A9, TOPREAL1:6;
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:2;
A12: p2 in LSeg (p1,p2) by RLTOPSP1:68;
then LSeg (p0,p2) c= L by A6, TOPREAL1:6;
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:6;
A13: PX1 /\ PX2 = {p0} by A6, TOPREAL1:8;
A14: R1 c= PX1 by XBOOLE_1:36;
A15: now :: thesis: not P c= R1
assume P c= R1 ; :: thesis: contradiction
then A16: p2 in R1 by A3;
p2 in PX2 by RLTOPSP1:68;
then p2 in PX1 /\ PX2 by A14, A16, XBOOLE_0:def 4;
hence contradiction by A3, A7, A13, TARSKI:def 1; :: thesis: verum
end;
A17: {p0} c= LSeg (p1,p0)
proof
let d be object ; :: according to TARSKI:def 3 :: thesis: ( not d in {p0} or d in LSeg (p1,p0) )
assume d in {p0} ; :: thesis: d in LSeg (p1,p0)
then d = p0 by TARSKI:def 1;
hence d in LSeg (p1,p0) by RLTOPSP1:68; :: thesis: verum
end;
A18: {p0} c= LSeg (p0,p2)
proof
let d be object ; :: according to TARSKI:def 3 :: thesis: ( not d in {p0} or d in LSeg (p0,p2) )
assume d in {p0} ; :: thesis: d in LSeg (p0,p2)
then d = p0 by TARSKI:def 1;
hence d in LSeg (p0,p2) by RLTOPSP1:68; :: thesis: verum
end;
PX2 is compact by COMPTS_1:19;
then PX2 is closed by A11, COMPTS_1:7;
then A19: Cl PX2 = PX2 by PRE_TOPC:22;
A20: Cl R2 c= Cl PX2 by PRE_TOPC:19, 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 ;
A22: PX1 /\ PX2 = {p0} by A6, TOPREAL1:8;
A23: R2 c= PX2 by XBOOLE_1:36;
A24: now :: thesis: not P c= R2
assume P c= R2 ; :: thesis: contradiction
then A25: p1 in R2 by A2;
p1 in PX1 by RLTOPSP1:68;
then p1 in PX1 /\ PX2 by A23, A25, XBOOLE_0:def 4;
hence contradiction by A2, A7, A13, TARSKI:def 1; :: thesis: verum
end;
PX1 is compact by COMPTS_1:19;
then PX1 is closed by A11, COMPTS_1:7;
then A26: Cl PX1 = PX1 by PRE_TOPC:22;
A27: L = (LSeg (p1,p0)) \/ (LSeg (p0,p2)) by A6, TOPREAL1:5
.= (((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 object ; :: according to TARSKI:def 3 :: thesis: ( not z in P or z in R1 \/ R2 )
assume A29: z in P ; :: thesis: z in R1 \/ R2
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: verum
end;
A30: Cl R1 c= Cl PX1 by PRE_TOPC:19, 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 ;
then A31: R1,R2 are_separated by A21, CONNSP_1:def 1;
PX is connected by A4, CONNSP_1:46;
hence contradiction by A31, A28, A15, A24, CONNSP_1:16; :: thesis: verum
end;
hence P = LSeg (p1,p2) by A1; :: thesis: verum