let P be Subset of (TOP-REAL 2); proj2 .: (Cl P) c= Cl (proj2 .: P)
let y be set ; TARSKI:def 3 ( not y in proj2 .: (Cl P) or y in Cl (proj2 .: P) )
assume
y in proj2 .: (Cl P)
; y in Cl (proj2 .: P)
then consider x being set such that
A1:
x in the carrier of (TOP-REAL 2)
and
A2:
x in Cl P
and
A3:
y = proj2 . x
by FUNCT_2:115;
reconsider x = x as Point of (TOP-REAL 2) by A1;
set r = proj2 . x;
for O being open Subset of REAL st y in O holds
not O /\ (proj2 .: P) is empty
proof
reconsider e =
x as
Point of
(Euclid 2) by TOPREAL3:13;
let O be
open Subset of
REAL ;
( y in O implies not O /\ (proj2 .: P) is empty )
assume
y in O
;
not O /\ (proj2 .: P) is empty
then consider g being
real number such that A4:
0 < g
and A5:
].((proj2 . x) - g),((proj2 . x) + g).[ c= O
by A3, RCOMP_1:40;
reconsider g =
g as
Real by XREAL_0:def 1;
reconsider B =
Ball e,
(g / 2) as
Subset of
(TOP-REAL 2) by TOPREAL3:13;
A6:
B is
open
by GOBOARD6:6;
e in B
by A4, TBSP_1:16, XREAL_1:141;
then
P meets B
by A2, A6, TOPS_1:39;
then
P /\ B <> {}
by XBOOLE_0:def 7;
then consider d being
Point of
(TOP-REAL 2) such that A7:
d in P /\ B
by SUBSET_1:10;
A8:
d in B
by A7, XBOOLE_0:def 4;
then
(x `2 ) - (g / 2) < d `2
by Th48;
then A9:
(proj2 . x) - (g / 2) < d `2
by PSCOMP_1:def 29;
d `2 < (x `2 ) + (g / 2)
by A8, Th48;
then A10:
d `2 < (proj2 . x) + (g / 2)
by PSCOMP_1:def 29;
d in P
by A7, XBOOLE_0:def 4;
then
proj2 . d in proj2 .: P
by FUNCT_2:43;
then A11:
d `2 in proj2 .: P
by PSCOMP_1:def 29;
A12:
g / 2
< g / 1
by A4, XREAL_1:78;
then
(proj2 . x) - g < (proj2 . x) - (g / 2)
by XREAL_1:17;
then A13:
(proj2 . x) - g < d `2
by A9, XXREAL_0:2;
(proj2 . x) + (g / 2) < (proj2 . x) + g
by A12, XREAL_1:8;
then A14:
d `2 < (proj2 . x) + g
by A10, XXREAL_0:2;
].((proj2 . x) - g),((proj2 . x) + g).[ = { t where t is Real : ( (proj2 . x) - g < t & t < (proj2 . x) + g ) }
by RCOMP_1:def 2;
then
d `2 in ].((proj2 . x) - g),((proj2 . x) + g).[
by A13, A14;
hence
not
O /\ (proj2 .: P) is
empty
by A5, A11, XBOOLE_0:def 4;
verum
end;
hence
y in Cl (proj2 .: P)
by A3, MEASURE6:99; verum