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:7;
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:60;
for p being Point of (Euclid 2) st p in C holds
ex r being real number st
( r > 0 & Ball p,r c= C )
proof
let p be
Point of
(Euclid 2);
( p in C implies ex r being real number st
( r > 0 & Ball p,r c= C ) )
assume A6:
p in C
;
ex r being real number st
( r > 0 & Ball p,r c= C )
then consider r being
real number such that A7:
r > 0
and A8:
Ball p,
r c= D
by A3, A5, TOPMETR:22;
reconsider r =
r as
Real by XREAL_0:def 1;
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:16;
A9:
p in E
by A7, GOBOARD6:4;
then A10:
E is
connected
by Th17;
B meets E
by A6, A9, XBOOLE_0:3;
hence
Ball p,
r c= C
by A2, A8, A10, GOBOARD9:6;
verum
end;
then
C is open
by TOPMETR:22;
hence
B is open
by A4, PRE_TOPC:60; verum