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
P is open
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 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
reconsider RR = R, PP = P as Subset of TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) ;
R is open by A1;
then A4: RR is open by PRE_TOPC:30;
now :: thesis: for u being Point of (Euclid 2) st u in P holds
ex r being Real st
( r > 0 & Ball (u,r) c= P )
let u be Point of (Euclid 2); :: thesis: ( u in P implies ex r being Real st
( r > 0 & Ball (u,r) c= P ) )
reconsider p2 = u as Point of (TOP-REAL 2) by TOPREAL3:8;
assume u in P ; :: thesis: ex r being Real 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 :: thesis: p2 in R
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, Th3;
hence p2 in R by A8; :: thesis: verum
end;
end;
end;
then consider r being Real such that
A9: r > 0 and
A10: Ball (u,r) c= RR by A4, Lm1, TOPMETR:15;
take r = r; :: thesis: ( r > 0 & Ball (u,r) c= P )
thus r > 0 by A9; :: thesis: Ball (u,r) c= P
reconsider r9 = r as Real ;
A11: p2 in Ball (u,r9) by A9, TBSP_1:11;
thus Ball (u,r) c= P :: thesis: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Ball (u,r) or x in P )
assume A12: x in Ball (u,r) ; :: thesis: x in P
then reconsider q = x as Point of (TOP-REAL 2) by A10, TARSKI:def 3;
now :: thesis: x in P
per cases ( q = p or q <> p ) ;
suppose q = p ; :: thesis: x in P
hence x in P by A3; :: thesis: verum
end;
suppose A13: q <> p ; :: thesis: x in P
A14: now :: thesis: ( q1 = p implies x in P )
assume q1 = p ; :: thesis: x in P
then p in Ball (u,r9) by A5, A9, TBSP_1:11;
then consider P2 being Subset of (TOP-REAL 2) such that
A15: P2 is_S-P_arc_joining p,q and
A16: P2 c= Ball (u,r9) by A12, A13, Th10;
reconsider P2 = P2 as Subset of (TOP-REAL 2) ;
P2 c= R by A10, A16;
hence x in P by A3, A15; :: thesis: verum
end;
now :: thesis: ( q1 <> p implies x in P )
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, A10, A11, A12, A13, Th23;
hence x in P by A3; :: thesis: verum
end;
hence x in P by A14; :: thesis: verum
end;
end;
end;
hence x in P ; :: thesis: verum
end;
end;
then PP is open by Lm1, TOPMETR:15;
hence P is open by PRE_TOPC:30; :: thesis: verum