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;

hence P is open by PRE_TOPC:30; :: thesis: verum

( 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 )

then
PP is open
by Lm1, TOPMETR:15;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

end;( 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) ;

end;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: contradictionend;

hence
contradiction
; :: thesis: verumper 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;

end;

( P1 is_S-P_arc_joining p,q & P1 c= R ) ) by A2, A6, A8, A9;

suppose A10:
q = p
; :: thesis: contradiction

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

end;

A11: now :: thesis: not q = p2

u in Ball (u,r9)
by A5, TBSP_1:11;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;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

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

hence
contradiction
by A4; :: thesis: verum
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;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

suppose A14:
ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p,q & P1 c= R ) ; :: thesis: contradiction

( P1 is_S-P_arc_joining p,q & P1 c= R ) ; :: thesis: contradiction

not p2 in P

end;proof

hence
contradiction
by A4; :: thesis: verum
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;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

hence P is open by PRE_TOPC:30; :: thesis: verum