let p be Point of (TOP-REAL 2); for P, R being Subset of (TOP-REAL 2) st R is being_Region & p in R & P = { q where q is Point of (TOP-REAL 2) : ( q = p or ex P1 being Subset of (TOP-REAL 2) st
( P1 is_S-P_arc_joining p,q & P1 c= R ) ) } holds
R c= P
let P, R be Subset of (TOP-REAL 2); ( R is being_Region & p in R & P = { q where q is Point of (TOP-REAL 2) : ( q = p or ex P1 being Subset of (TOP-REAL 2) st
( P1 is_S-P_arc_joining p,q & P1 c= R ) ) } implies R c= P )
assume that
A1:
R is being_Region
and
A2:
p in R
and
A3:
P = { q where q is Point of (TOP-REAL 2) : ( q = p or ex P1 being Subset of (TOP-REAL 2) st
( P1 is_S-P_arc_joining p,q & P1 c= R ) ) }
; R c= P
A4:
p in P
by A3;
set P2 = R \ P;
reconsider P22 = R \ P as Subset of (TOP-REAL 2) ;
A5:
[#] ((TOP-REAL 2) | R) = R
by PRE_TOPC:def 5;
then reconsider P11 = P, P12 = P22 as Subset of ((TOP-REAL 2) | R) by A2, A3, Th26, XBOOLE_1:36;
P \/ (R \ P) = P \/ R
by XBOOLE_1:39;
then A6:
[#] ((TOP-REAL 2) | R) = P11 \/ P12
by A5, XBOOLE_1:12;
then
R \ P = { q where q is Point of (TOP-REAL 2) : ( q <> p & q in R & ( for P1 being Subset of (TOP-REAL 2) holds
( not P1 is_S-P_arc_joining p,q or not P1 c= R ) ) ) }
by TARSKI:2;
then
P22 is open
by A1, Th24;
then A11:
P22 in the topology of (TOP-REAL 2)
by PRE_TOPC:def 2;
reconsider R9 = R as non empty Subset of (TOP-REAL 2) by A2;
R is connected
by A1;
then A12:
(TOP-REAL 2) | R9 is connected
by CONNSP_1:def 3;
P is open
by A1, A2, A3, Th25;
then A13:
P in the topology of (TOP-REAL 2)
by PRE_TOPC:def 2;
P11 = P /\ ([#] ((TOP-REAL 2) | R))
by XBOOLE_1:28;
then
P11 in the topology of ((TOP-REAL 2) | R)
by A13, PRE_TOPC:def 4;
then A14:
P11 is open
by PRE_TOPC:def 2;
P12 = P22 /\ ([#] ((TOP-REAL 2) | R))
by XBOOLE_1:28;
then
P12 in the topology of ((TOP-REAL 2) | R)
by A11, PRE_TOPC:def 4;
then A15:
P12 is open
by PRE_TOPC:def 2;
A16:
P11 misses P12
by XBOOLE_1:79;
then
P11 /\ P12 = {} ((TOP-REAL 2) | R)
;
then
R \ P = {}
by A4, A12, A16, A6, A14, A15, CONNSP_1:11;
hence
R c= P
by XBOOLE_1:37; verum