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:7;
A4:
TOP-REAL 2 = TopSpaceMetr (Euclid 2)
by EUCLID:def 8;
reconsider C = B, D = A as Subset of (TopSpaceMetr (Euclid 2)) by EUCLID:def 8;
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);
:: thesis: ( p in C implies ex r being real number st
( r > 0 & Ball p,r c= C ) )
assume A5:
p in C
;
:: thesis: ex r being real number st
( r > 0 & Ball p,r c= C )
then consider r being
real number such that A6:
r > 0
and A7:
Ball p,
r c= D
by A1, A3, A4, TOPMETR:22;
reconsider r =
r as
Real by XREAL_0:def 1;
take
r
;
:: thesis: ( r > 0 & Ball p,r c= C )
thus
r > 0
by A6;
:: thesis: Ball p,r c= C
reconsider E =
Ball p,
r as
Subset of
(TOP-REAL 2) by A4, TOPMETR:16;
A8:
p in E
by A6, GOBOARD6:4;
then A9:
B meets E
by A5, XBOOLE_0:3;
E is
connected
by A8, Th17;
hence
Ball p,
r c= C
by A2, A7, A9, GOBOARD9:6;
:: thesis: verum
end;
hence
B is open
by A4, TOPMETR:22; :: thesis: verum