let R, P be Subset of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st R is being_Region & 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 ) ) ) } holds
P is open
let p be Point of (TOP-REAL 2); :: thesis: ( R is being_Region & 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 ) ) ) } implies P is open )
assume that
A1: R is being_Region and
A2: 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 ) ) ) } ; :: thesis: P is open
A3: R is open by A1, Def3;
X: TopStruct(# the carrier of (TOP-REAL 2),the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) by EUCLID:def 8;
reconsider RR = R, PP = P as Subset of TopStruct(# the carrier of (TOP-REAL 2),the topology of (TOP-REAL 2) #) ;
Y: RR is open by A3, PRE_TOPC:60;

now

let u be Point of (Euclid 2); :: thesis: ( u in P implies ex r being real number st
( r > 0 & Ball u,r c= P ) )
reconsider p2 = u as Point of (TOP-REAL 2) by TOPREAL3:13;
assume A4: u in P ; :: thesis: ex r being real number st
( r > 0 & Ball u,r c= P )
then ex q1 being Point of (TOP-REAL 2) st
( q1 = u & q1 <> p & q1 in R & ( for P1 being Subset of (TOP-REAL 2) holds
( not P1 is_S-P_arc_joining p,q1 or not P1 c= R ) ) ) by A2;
then consider r being real number such that
A5: ( r > 0 & Ball u,r c= RR ) by A3, Lm1, X, Y, TOPMETR:22;
reconsider r' = r as Real by XREAL_0:def 1;
A6: p2 in Ball u,r' by A5, TBSP_1:16;
take r = r; :: thesis: ( r > 0 & Ball u,r c= P )
thus r > 0 by A5; :: thesis: Ball u,r c= P
thus Ball u,r c= P :: thesis: verum

proof

assume not Ball u,r c= P ; :: thesis: contradiction
then consider x being set such that
A7: ( x in Ball u,r & not x in P ) by TARSKI:def 3;
x in R by A5, A7;
then reconsider q = x as Point of (TOP-REAL 2) ;

now

per cases ( q = p or ex P1 being Subset of (TOP-REAL 2) st
( P1 is_S-P_arc_joining p,q & P1 c= R ) ) by A2, A5, A7;

suppose A8: q = p ; :: thesis: contradiction

now

assume A9: q = p2 ; :: thesis: contradiction
ex p3 being Point of (TOP-REAL 2) st
( p3 = p2 & p3 <> p & p3 in R & ( for P1 being Subset of (TOP-REAL 2) holds
( not P1 is_S-P_arc_joining p,p3 or not P1 c= R ) ) ) by A2, A4;
hence contradiction by A8, A9; :: thesis: verum

end;

then ( q <> p2 & u in Ball u,r' ) by A5, TBSP_1:16;
then consider P2 being Subset of (TOP-REAL 2) such that
A10: ( P2 is_S-P_arc_joining q,p2 & P2 c= Ball u,r' ) by A7, Th11;
not p2 in P

proof

assume p2 in P ; :: thesis: contradiction
then ex q4 being Point of (TOP-REAL 2) st
( q4 = p2 & q4 <> p & q4 in R & ( for P1 being Subset of (TOP-REAL 2) holds
( not P1 is_S-P_arc_joining p,q4 or not P1 c= R ) ) ) by A2;
hence contradiction by A5, A8, A10, XBOOLE_1:1; :: thesis: verum

end;

hence contradiction by A4; :: thesis: verum

end;

suppose A11: ex P1 being Subset of (TOP-REAL 2) st
( P1 is_S-P_arc_joining p,q & P1 c= R ) ; :: thesis: contradiction

not p2 in P

proof

assume p2 in P ; :: thesis: contradiction
then ex q4 being Point of (TOP-REAL 2) st
( q4 = p2 & q4 <> p & q4 in R & ( for P1 being Subset of (TOP-REAL 2) holds
( not P1 is_S-P_arc_joining p,q4 or not P1 c= R ) ) ) by A2;
hence contradiction by A5, A6, A7, A11, Th24; :: thesis: verum

end;

hence contradiction by A4; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

then PP is open by Lm1, TOPMETR:22;
hence P is open by PRE_TOPC:60; :: thesis: verum