let P, R 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
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 A3: 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 A4: u in P ; :: thesis: ex r being Real 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 such that
A5: r > 0 and
A6: Ball (u,r) c= RR by A3, Lm1, TOPMETR:15;
take r = r; :: thesis: ( r > 0 & Ball (u,r) c= P )
thus r > 0 by A5; :: thesis: Ball (u,r) c= P
reconsider r9 = r as Real ;
A7: p2 in Ball (u,r9) by A5, TBSP_1:11;
thus Ball (u,r) c= P :: thesis: verum
proof
assume not Ball (u,r) c= P ; :: thesis: contradiction
then consider x being object such that
A8: x in Ball (u,r) and
A9: not x in P ;
x in R by A6, A8;
then reconsider q = x as Point of (TOP-REAL 2) ;
now :: thesis: contradiction
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, A6, A8, A9;
suppose A10: q = p ; :: thesis: contradiction
A11: now :: thesis: not q = p2
assume A12: 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 A10, A12; :: thesis: verum
end;
u in Ball (u,r9) by A5, TBSP_1:11;
then A13: ex P2 being Subset of (TOP-REAL 2) st
( P2 is_S-P_arc_joining q,p2 & P2 c= Ball (u,r9) ) by A8, A11, Th10;
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 A6, A10, A13, XBOOLE_1:1; :: thesis: verum
end;
hence contradiction by A4; :: thesis: verum
end;
suppose A14: 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 A6, A7, A8, A14, Th23; :: 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:15;
hence P is open by PRE_TOPC:30; :: thesis: verum