let X be LinearTopSpace; :: thesis: for V being a_neighborhood of 0. X ex W being a_neighborhood of 0. X st Cl W c= V
let V be a_neighborhood of 0. X; :: thesis: ex W being a_neighborhood of 0. X st Cl W c= V
set B = { U where U is a_neighborhood of 0. X : verum } ;
{ U where U is a_neighborhood of 0. X : verum } c= bool the carrier of X
proof
let A be object ; :: according to TARSKI:def 3 :: thesis: ( not A in { U where U is a_neighborhood of 0. X : verum } or A in bool the carrier of X )
assume A in { U where U is a_neighborhood of 0. X : verum } ; :: thesis: A in bool the carrier of X
then ex U being a_neighborhood of 0. X st A = U ;
hence A in bool the carrier of X ; :: thesis: verum
end;
then { U where U is a_neighborhood of 0. X : verum } is local_base of X by Th44;
then consider W being a_neighborhood of 0. X such that
W in { U where U is a_neighborhood of 0. X : verum } and
A1: Cl W c= V by Th58;
take W ; :: thesis: Cl W c= V
thus Cl W c= V by A1; :: thesis: verum