let P, R 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 TopStruct(# the carrier of (), the topology of () #) ;
R is open by A1;
then A3: RR is open by PRE_TOPC:30;
now :: thesis: for u being Point of () st u in P holds
ex r being Real st
( r > 0 & Ball (u,r) c= P )
let u be Point of (); :: thesis: ( u in P implies ex r being Real st
( r > 0 & Ball (u,r) c= P ) )

reconsider p2 = u as Point of () 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 () 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 such that
A5: r > 0 and
A6: Ball (u,r) c= RR by ;
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 ;
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 () ;
now :: thesis: contradiction
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 :: thesis: not q = p2
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,r9) by ;
then A13: ex P2 being Subset of () st
( P2 is_S-P_arc_joining q,p2 & P2 c= Ball (u,r9) ) by ;
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, Th23; :: thesis: verum
end;
hence contradiction by A4; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
end;
then PP is open by ;
hence P is open by PRE_TOPC:30; :: thesis: verum