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
P is open
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 P is open )
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: P is open
A4: 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 A4, 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 u in P ; :: thesis: ex r being real number st
( r > 0 & Ball u,r c= P )
then consider q1 being Point of (TOP-REAL 2) such that
A5: q1 = u and
A6: ( q1 = p or ex P1 being Subset of (TOP-REAL 2) st
( P1 is_S-P_arc_joining p,q1 & P1 c= R ) ) by A3;

now

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

suppose q1 = p ; :: thesis: p2 in R

hence p2 in R by A2, A5; :: thesis: verum

end;

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

then consider P2 being Subset of (TOP-REAL 2) such that
A7: P2 is_S-P_arc_joining p,q1 and
A8: P2 c= R ;
p2 in P2 by A5, A7, Th4;
hence p2 in R by A8; :: thesis: verum

end;

end;

end;

then consider r being real number such that
A9: ( r > 0 & Ball u,r c= RR ) by A4, Lm1, X, Y, TOPMETR:22;
take r = r; :: thesis: ( r > 0 & Ball u,r c= P )
reconsider r' = r as Real by XREAL_0:def 1;
A10: p2 in Ball u,r' by A9, TBSP_1:16;
thus r > 0 by A9; :: thesis: Ball u,r c= P
thus Ball u,r c= P :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Ball u,r or x in P )
assume A11: x in Ball u,r ; :: thesis: x in P
then reconsider q = x as Point of (TOP-REAL 2) by A9, TARSKI:def 3;

now

per cases ( q = p or q <> p ) ;

suppose q = p ; :: thesis: x in P

hence x in P by A3; :: thesis: verum

end;

suppose A12: q <> p ; :: thesis: x in P

A13: now

assume q1 <> p ; :: thesis: x in P
then ex P1 being Subset of (TOP-REAL 2) st
( P1 is_S-P_arc_joining p,q & P1 c= R ) by A5, A6, A9, A10, A11, A12, Th24;
hence x in P by A3; :: thesis: verum

end;

now

assume q1 = p ; :: thesis: x in P
then p in Ball u,r' by A5, A9, TBSP_1:16;
then consider P2 being Subset of (TOP-REAL 2) such that
A14: ( P2 is_S-P_arc_joining p,q & P2 c= Ball u,r' ) by A11, A12, Th11;
reconsider P2 = P2 as Subset of (TOP-REAL 2) ;
( P2 is_S-P_arc_joining p,q & P2 c= R ) by A9, A14, XBOOLE_1:1;
hence x in P by A3; :: thesis: verum

end;

hence x in P by A13; :: thesis: verum

end;

end;

end;

hence x in P ; :: thesis: verum

end;

end;

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