let p be Point of (TOP-REAL 2); :: thesis: 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); :: 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
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;

now :: thesis: for x being object holds
( 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 ) ) ) } )

let x be object ; :: 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 ) ) ) } )

A7: now :: thesis: ( x in R \ P implies 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 ) ) ) } )

assume A8: 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 reconsider q2 = x as Point of (TOP-REAL 2) ;
not x in P by A8, XBOOLE_0:def 5;
then A9: ( q2 <> p & ( 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;
q2 in R by A8, XBOOLE_0:def 5;
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 ) ) ) } by A9; :: thesis: verum

end;

now :: 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 ) ) ) } implies x in R \ P )

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 A10: 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 not x in P by A3;
hence x in R \ P by A10, 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 A7; :: thesis: verum

end;

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; :: thesis: verum