let A, B be Subset of (); :: 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 ;
A4: TopStruct(# the U1 of (), the topology of () #) = TopSpaceMetr () by EUCLID:def 8;
then reconsider C = B, D = A as Subset of () ;
A5: D is open by ;
for p being Point of () st p in C holds
ex r being Real st
( r > 0 & Ball (p,r) c= C )
proof
let p be Point of (); :: 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 ;
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 () by ;
A9: p in E by ;
then A10: E is connected by Th7;
B meets E by ;
hence Ball (p,r) c= C by ; :: thesis: verum
end;
then C is open by TOPMETR:15;
hence B is open by ; :: thesis: verum