let X be LinearTopSpace; for A being Subset of X holds Cl A = meet { (A + V) where V is a_neighborhood of 0. X : verum }
let A be Subset of X; Cl A = meet { (A + V) where V is a_neighborhood of 0. X : verum }
set AV = { (A + V) where V is a_neighborhood of 0. X : verum } ;
set V = the a_neighborhood of 0. X;
A1:
for x being Point of X
for V being a_neighborhood of 0. X holds
( A meets x + (Int V) iff x in A + ((- 1) * (Int V)) )
{ (A + V) where V is a_neighborhood of 0. X : verum } c= bool the carrier of X
then reconsider AV9 = { (A + V) where V is a_neighborhood of 0. X : verum } as Subset-Family of X ;
A9:
for x being Point of X holds
( x in Cl A iff for V being a_neighborhood of 0. X holds A meets x + (Int V) )
A15:
A + the a_neighborhood of 0. X in { (A + V) where V is a_neighborhood of 0. X : verum }
;
thus
Cl A c= meet { (A + V) where V is a_neighborhood of 0. X : verum }
XBOOLE_0:def 10 meet { (A + V) where V is a_neighborhood of 0. X : verum } c= Cl Aproof
let x be
object ;
TARSKI:def 3 ( not x in Cl A or x in meet { (A + V) where V is a_neighborhood of 0. X : verum } )
assume A16:
x in Cl A
;
x in meet { (A + V) where V is a_neighborhood of 0. X : verum }
then reconsider x =
x as
Point of
X ;
now for Y being set st Y in { (A + V) where V is a_neighborhood of 0. X : verum } holds
x in Ylet Y be
set ;
( Y in { (A + V) where V is a_neighborhood of 0. X : verum } implies x in Y )assume
Y in { (A + V) where V is a_neighborhood of 0. X : verum }
;
x in Ythen consider V being
a_neighborhood of
0. X such that A17:
Y = A + V
;
A18:
A + V = { (a + v) where a, v is Point of X : ( a in A & v in V ) }
by RUSUB_4:def 9;
A19:
(- 1) * V is
a_neighborhood of
0. X
by Th55;
then
A meets x + (Int ((- 1) * V))
by A9, A16;
then
(
A + ((- 1) * (Int ((- 1) * V))) = { (a + v) where a, v is Point of X : ( a in A & v in (- 1) * (Int ((- 1) * V)) ) } &
x in A + ((- 1) * (Int ((- 1) * V))) )
by A1, A19, RUSUB_4:def 9;
then consider a,
v being
Point of
X such that A20:
(
x = a + v &
a in A )
and A21:
v in (- 1) * (Int ((- 1) * V))
;
consider v9 being
Point of
X such that A22:
v = (- 1) * v9
and A23:
v9 in Int ((- 1) * V)
by A21;
Int ((- 1) * V) c= (- 1) * V
by TOPS_1:16;
then
v9 in (- 1) * V
by A23;
then consider v99 being
Point of
X such that A24:
v9 = (- 1) * v99
and A25:
v99 in V
;
v =
((- 1) * (- 1)) * v99
by A22, A24, RLVECT_1:def 7
.=
v99
by RLVECT_1:def 8
;
hence
x in Y
by A17, A18, A20, A25;
verum end;
hence
x in meet { (A + V) where V is a_neighborhood of 0. X : verum }
by A15, SETFAM_1:def 1;
verum
end;
let x be object ; TARSKI:def 3 ( not x in meet { (A + V) where V is a_neighborhood of 0. X : verum } or x in Cl A )
assume A26:
x in meet { (A + V) where V is a_neighborhood of 0. X : verum }
; x in Cl A
meet AV9 c= the carrier of X
;
then reconsider x = x as Point of X by A26;
hence
x in Cl A
by A9; verum