let A, B be Subset of (TOP-REAL 2); ( 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
; 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
let p be
Point of
(Euclid 2);
( p in C implies ex r being Real st
( r > 0 & Ball (p,r) c= C ) )
assume A6:
p in C
;
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
;
( r > 0 & Ball (p,r) c= C )
thus
r > 0
by A7;
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;
verum
end;
then
C is open
by TOPMETR:15;
hence
B is open
by A4, PRE_TOPC:30; verum