let P be Subset of (TOP-REAL 2); :: thesis: proj1 .: (Cl P) c= Cl (proj1 .: P)
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in proj1 .: (Cl P) or y in Cl (proj1 .: P) )
assume
y in proj1 .: (Cl P)
; :: thesis: y in Cl (proj1 .: 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 = proj1 . x
by FUNCT_2:115;
reconsider x = x as Point of (TOP-REAL 2) by A1;
set r = proj1 . x;
for O being open Subset of REAL st y in O holds
not O /\ (proj1 .: P) is empty
proof
let O be
open Subset of
REAL ;
:: thesis: ( y in O implies not O /\ (proj1 .: P) is empty )
assume
y in O
;
:: thesis: not O /\ (proj1 .: P) is empty
then consider g being
real number such that A4:
0 < g
and A5:
].((proj1 . x) - g),((proj1 . x) + g).[ c= O
by A3, RCOMP_1:40;
reconsider g =
g as
Real by XREAL_0:def 1;
reconsider e =
x as
Point of
(Euclid 2) by TOPREAL3:13;
reconsider B =
Ball e,
(g / 2) as
Subset of
(TOP-REAL 2) by TOPREAL3:13;
A6:
B is
open
by GOBOARD6:6;
g / 2
> 0
by A4, XREAL_1:141;
then
e in B
by TBSP_1:16;
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;
d in P
by A7, XBOOLE_0:def 4;
then
proj1 . d in proj1 .: P
by FUNCT_2:43;
then A8:
d `1 in proj1 .: P
by PSCOMP_1:def 28;
A9:
].((proj1 . x) - g),((proj1 . x) + g).[ = { t where t is Real : ( (proj1 . x) - g < t & t < (proj1 . x) + g ) }
by RCOMP_1:def 2;
d in B
by A7, XBOOLE_0:def 4;
then
(
(x `1 ) - (g / 2) < d `1 &
d `1 < (x `1 ) + (g / 2) )
by Th47;
then A10:
(
(proj1 . x) - (g / 2) < d `1 &
d `1 < (proj1 . x) + (g / 2) )
by PSCOMP_1:def 28;
g / 2
< g / 1
by A4, XREAL_1:78;
then
(
(proj1 . x) - g < (proj1 . x) - (g / 2) &
(proj1 . x) + (g / 2) < (proj1 . x) + g )
by XREAL_1:8, XREAL_1:17;
then
(
(proj1 . x) - g < d `1 &
d `1 < (proj1 . x) + g )
by A10, XXREAL_0:2;
then
d `1 in ].((proj1 . x) - g),((proj1 . x) + g).[
by A9;
hence
not
O /\ (proj1 .: P) is
empty
by A5, A8, XBOOLE_0:def 4;
:: thesis: verum
end;
hence
y in Cl (proj1 .: P)
by A3, PSCOMP_1:38; :: thesis: verum