let P be Subset of (TOP-REAL 2); proj2 .: (Cl P) c= Cl (proj2 .: P)
let y be object ; 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 object 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:64;
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:8;
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 such that A4:
0 < g
and A5:
].((proj2 . x) - g),((proj2 . x) + g).[ c= O
by A3, RCOMP_1:19;
reconsider g =
g as
Real ;
reconsider B =
Ball (
e,
(g / 2)) as
Subset of
(TOP-REAL 2) by TOPREAL3:8;
A6:
B is
open
by GOBOARD6:3;
e in B
by A4, TBSP_1:11, XREAL_1:139;
then
P meets B
by A2, A6, TOPS_1:12;
then
P /\ B <> {}
;
then consider d being
Point of
(TOP-REAL 2) such that A7:
d in P /\ B
by SUBSET_1:4;
A8:
d in B
by A7, XBOOLE_0:def 4;
then
(x `2) - (g / 2) < d `2
by Th38;
then A9:
(proj2 . x) - (g / 2) < d `2
by PSCOMP_1:def 6;
d `2 < (x `2) + (g / 2)
by A8, Th38;
then A10:
d `2 < (proj2 . x) + (g / 2)
by PSCOMP_1:def 6;
d in P
by A7, XBOOLE_0:def 4;
then
proj2 . d in proj2 .: P
by FUNCT_2:35;
then A11:
d `2 in proj2 .: P
by PSCOMP_1:def 6;
A12:
g / 2
< g / 1
by A4, XREAL_1:76;
then
(proj2 . x) - g < (proj2 . x) - (g / 2)
by XREAL_1:15;
then A13:
(proj2 . x) - g < d `2
by A9, XXREAL_0:2;
(proj2 . x) + (g / 2) < (proj2 . x) + g
by A12, XREAL_1:6;
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:63; verum