let R, P be Subset of ; :: thesis: for p being Point of st R is being_Region & P = { q where q is Point of : ( q <> p & q in R & ( for P1 being Subset of holds
( not P1 is_S-P_arc_joining p,q or not P1 c= R ) ) ) } holds
P is open
let p be Point of ; :: thesis: ( R is being_Region & P = { q where q is Point of : ( q <> p & q in R & ( for P1 being Subset of 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 : ( q <> p & q in R & ( for P1 being Subset of 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 ;
R is open by A1, Def3;
then A3: RR is open by PRE_TOPC:60;
now
let u be Point of ; :: thesis: ( u in P implies ex r being real number st
( r > 0 & Ball u,r c= P ) )
reconsider p2 = u as Point of 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 st
( q1 = u & q1 <> p & q1 in R & ( for P1 being Subset of 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 and
A6: Ball u,r c= RR by A3, Lm1, TOPMETR:22;
take r = r; :: thesis: ( r > 0 & Ball u,r c= P )
thus r > 0 by A5; :: thesis: Ball u,r c= P
reconsider r' = r as Real by XREAL_0:def 1;
A7: p2 in Ball u,r' by A5, TBSP_1:16;
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
A8: x in Ball u,r and
A9: not x in P by TARSKI:def 3;
x in R by A6, A8;
then reconsider q = x as Point of ;
now
per cases ( q = p or ex P1 being Subset of 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
assume A12: q = p2 ; :: thesis: contradiction
ex p3 being Point of st
( p3 = p2 & p3 <> p & p3 in R & ( for P1 being Subset of 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,r' by A5, TBSP_1:16;
then A13: ex P2 being Subset of st
( P2 is_S-P_arc_joining q,p2 & P2 c= Ball u,r' ) by A8, A11, Th11;
not p2 in P
proof
assume p2 in P ; :: thesis: contradiction
then ex q4 being Point of st
( q4 = p2 & q4 <> p & q4 in R & ( for P1 being Subset of 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 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 st
( q4 = p2 & q4 <> p & q4 in R & ( for P1 being Subset of holds
( not P1 is_S-P_arc_joining p,q4 or not P1 c= R ) ) ) by A2;
hence contradiction by A6, A7, A8, A14, 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