let X be LinearTopSpace; :: thesis: for B being local_base of X
for V being a_neighborhood of 0. X ex W being a_neighborhood of 0. X st
( W in B & Cl W c= V )
let B be local_base of X; :: thesis: for V being a_neighborhood of 0. X ex W being a_neighborhood of 0. X st
( W in B & Cl W c= V )
let V be a_neighborhood of 0. X; :: thesis: ex W being a_neighborhood of 0. X st
( W in B & Cl W c= V )
set C = (Int V) ` ;
set K = {(0. X)};
0. X in Int V by CONNSP_2:def 1;
then not 0. X in (Int V) ` by XBOOLE_0:def 5;
then consider P being a_neighborhood of 0. X such that
A1: {(0. X)} + P misses ((Int V) `) + P by Th57, ZFMISC_1:50;
A2: 0. X in Int P by CONNSP_2:def 1;
then reconsider P9 = Int P as open a_neighborhood of 0. X by CONNSP_2:3;
( {(0. X)} + P9 c= {(0. X)} + P & ((Int V) `) + P9 c= ((Int V) `) + P ) by Lm3, TOPS_1:16;
then {(0. X)} + P9 misses ((Int V) `) + P9 by A1, XBOOLE_1:64;
then Cl ({(0. X)} + P9) misses ((Int V) `) + P9 by TSEP_1:36;
then Cl ({(0. X)} + P9) misses (Int V) ` by A2, Th12, XBOOLE_1:63;
then Cl P9 misses (Int V) ` by CONVEX1:35;
then A3: Cl P9 c= Int V by SUBSET_1:24;
consider W being a_neighborhood of 0. X such that
A4: W in B and
A5: W c= P9 by YELLOW13:def 2;
take W ; :: thesis: ( W in B & Cl W c= V )
thus W in B by A4; :: thesis: Cl W c= V
A6: Cl W c= Cl P9 by A5, PRE_TOPC:19;
Int V c= V by TOPS_1:16;
then Cl P9 c= V by A3;
hence Cl W c= V by A6; :: thesis: verum