let A, B be Subset of (TOP-REAL 2); :: thesis: ( A is open & B is_a_component_of A implies B is open )

assume that

A1: A is open and

A2: B is_a_component_of A ; :: thesis: B is open

A3: B c= A by A2, SPRECT_1:5;

A4: TopStruct(# the U1 of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) by EUCLID:def 8;

then reconsider C = B, D = A as Subset of (TopSpaceMetr (Euclid 2)) ;

A5: D is open by A1, A4, PRE_TOPC:30;

for p being Point of (Euclid 2) st p in C holds

ex r being Real st

( r > 0 & Ball (p,r) c= C )

hence B is open by A4, PRE_TOPC:30; :: thesis: verum

assume that

A1: A is open and

A2: B is_a_component_of A ; :: thesis: B is open

A3: B c= A by A2, SPRECT_1:5;

A4: TopStruct(# the U1 of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) by EUCLID:def 8;

then reconsider C = B, D = A as Subset of (TopSpaceMetr (Euclid 2)) ;

A5: D is open by A1, A4, PRE_TOPC:30;

for p being Point of (Euclid 2) st p in C holds

ex r being Real st

( r > 0 & Ball (p,r) c= C )

proof

then
C is open
by TOPMETR:15;
let p be Point of (Euclid 2); :: thesis: ( p in C implies ex r being Real st

( r > 0 & Ball (p,r) c= C ) )

assume A6: p in C ; :: thesis: ex r being Real st

( r > 0 & Ball (p,r) c= C )

then consider r being Real such that

A7: r > 0 and

A8: Ball (p,r) c= D by A3, A5, TOPMETR:15;

reconsider r = r as Real ;

take r ; :: thesis: ( r > 0 & Ball (p,r) c= C )

thus r > 0 by A7; :: thesis: Ball (p,r) c= C

reconsider E = Ball (p,r) as Subset of (TOP-REAL 2) by A4, TOPMETR:12;

A9: p in E by A7, GOBOARD6:1;

then A10: E is connected by Th7;

B meets E by A6, A9, XBOOLE_0:3;

hence Ball (p,r) c= C by A2, A8, A10, GOBOARD9:4; :: thesis: verum

end;( r > 0 & Ball (p,r) c= C ) )

assume A6: p in C ; :: thesis: ex r being Real st

( r > 0 & Ball (p,r) c= C )

then consider r being Real such that

A7: r > 0 and

A8: Ball (p,r) c= D by A3, A5, TOPMETR:15;

reconsider r = r as Real ;

take r ; :: thesis: ( r > 0 & Ball (p,r) c= C )

thus r > 0 by A7; :: thesis: Ball (p,r) c= C

reconsider E = Ball (p,r) as Subset of (TOP-REAL 2) by A4, TOPMETR:12;

A9: p in E by A7, GOBOARD6:1;

then A10: E is connected by Th7;

B meets E by A6, A9, XBOOLE_0:3;

hence Ball (p,r) c= C by A2, A8, A10, GOBOARD9:4; :: thesis: verum

hence B is open by A4, PRE_TOPC:30; :: thesis: verum