let X be LinearTopSpace; :: thesis: for x being Point of X
for V being Subset of X holds x + (Cl V) = Cl (x + V)
let x be Point of X; :: thesis: for V being Subset of X holds x + (Cl V) = Cl (x + V)
let V be Subset of X; :: thesis: x + (Cl V) = Cl (x + V)
thus x + (Cl V) c= Cl (x + V) :: according to XBOOLE_0:def 10 :: thesis: Cl (x + V) c= x + (Cl V)

proof

let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in x + (Cl V) or v in Cl (x + V) )
assume A1: v in x + (Cl V) ; :: thesis: v in Cl (x + V)
then reconsider v = v as Point of X ;

now :: thesis: for G being Subset of X st G is open & v in G holds
x + V meets G

A2: x + (Cl V) = { (x + u) where u is Point of X : u in Cl V } by RUSUB_4:def 8;
A3: x + V = { (x + u) where u is Point of X : u in V } by RUSUB_4:def 8;
let G be Subset of X; :: thesis: ( G is open & v in G implies x + V meets G )
assume that
A4: G is open and
A5: v in G ; :: thesis: x + V meets G
A6: (- x) + G = { ((- x) + u) where u is Point of X : u in G } by RUSUB_4:def 8;
then A7: (- x) + v in (- x) + G by A5;
consider u being Point of X such that
A8: v = x + u and
A9: u in Cl V by A1, A2;
(- x) + v = ((- x) + x) + u by A8, RLVECT_1:def 3
.= (0. X) + u by RLVECT_1:5
.= u ;
then V meets (- x) + G by A4, A9, A7, PRE_TOPC:24;
then consider z being object such that
A10: z in V and
A11: z in (- x) + G by XBOOLE_0:3;
reconsider z = z as Point of X by A10;
consider w being Point of X such that
A12: z = (- x) + w and
A13: w in G by A6, A11;
A14: x + z in x + V by A3, A10;
x + z = (x + (- x)) + w by A12, RLVECT_1:def 3
.= (0. X) + w by RLVECT_1:5
.= w ;
hence x + V meets G by A13, A14, XBOOLE_0:3; :: thesis: verum

end;

hence v in Cl (x + V) by PRE_TOPC:24; :: thesis: verum

end;

x + V c= x + (Cl V) by Th8, PRE_TOPC:18;
hence Cl (x + V) c= x + (Cl V) by TOPS_1:5; :: thesis: verum