let p be Point of (TOP-REAL 2); :: thesis: for R, P 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 R, P be Subset of (TOP-REAL 2); :: thesis: ( 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 ) ) } ; :: thesis: R c= P
reconsider R' = R as non empty Subset of (TOP-REAL 2) by A2;
set P2 = R \ P;
A5: R \ P c= R by XBOOLE_1:36;

now

let x be set ; :: thesis: ( x in R \ P iff x in { 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 ) ) ) } )

A6: now

assume A7: x in R \ P ; :: thesis: x in { 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 ) ) ) }
then A8: ( x in R & not x in P ) by XBOOLE_0:def 5;
reconsider q2 = x as Point of (TOP-REAL 2) by A7;
( q2 <> p & q2 in R & ( for P1 being Subset of (TOP-REAL 2) holds
( not P1 is_S-P_arc_joining p,q2 or not P1 c= R ) ) ) by A3, A8;
hence x in { 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 ) ) ) } ; :: thesis: verum

end;

now

assume x in { 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 ) ) ) } ; :: thesis: x in R \ P
then A9: ex q3 being Point of (TOP-REAL 2) st
( q3 = x & q3 <> p & q3 in R & ( for P1 being Subset of (TOP-REAL 2) holds
( not P1 is_S-P_arc_joining p,q3 or not P1 c= R ) ) ) ;
then for q being Point of (TOP-REAL 2) holds
( not q = x or ( not q = p & ( for P1 being Subset of (TOP-REAL 2) holds
( not P1 is_S-P_arc_joining p,q or not P1 c= R ) ) ) ) ;
then ( x in R & not x in P ) by A3, A9;
hence x in R \ P by XBOOLE_0:def 5; :: thesis: verum

end;

hence ( x in R \ P iff x in { 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 A6; :: thesis: verum

end;

then A10: 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;
reconsider P22 = R \ P as Subset of (TOP-REAL 2) ;
A11: P22 is open by A1, A10, Th25;
A12: P is open by A1, A2, A3, Th26;
A13: p in P by A3;
R is connected by A1, Def3;
then A14: (TOP-REAL 2) | R' is connected by CONNSP_1:def 3;
A15: [#] ((TOP-REAL 2) | R) = R by PRE_TOPC:def 10;
then reconsider P11 = P, P12 = P22 as Subset of ((TOP-REAL 2) | R) by A2, A3, A5, Th27;
A16: P11 misses P12 by XBOOLE_1:79;
then A17: P11 /\ P12 = {} ((TOP-REAL 2) | R) by XBOOLE_0:def 7;
P \/ (R \ P) = P \/ R by XBOOLE_1:39;
then A18: [#] ((TOP-REAL 2) | R) = P11 \/ P12 by A15, XBOOLE_1:12;
A19: ( P22 in the topology of (TOP-REAL 2) & P in the topology of (TOP-REAL 2) ) by A11, A12, PRE_TOPC:def 5;
( P11 = P /\ ([#] ((TOP-REAL 2) | R)) & P12 = P22 /\ ([#] ((TOP-REAL 2) | R)) ) by XBOOLE_1:28;
then ( P11 in the topology of ((TOP-REAL 2) | R) & P12 in the topology of ((TOP-REAL 2) | R) ) by A19, PRE_TOPC:def 9;
then ( P11 is open & P12 is open ) by PRE_TOPC:def 5;
then R \ P = {} by A13, A14, A16, A17, A18, CONNSP_1:12;
hence R c= P by XBOOLE_1:37; :: thesis: verum