let X be LinearTopSpace; :: thesis: for a being Real
for x being Point of X
for V being a_neighborhood of a * x ex r being positive Real ex W being a_neighborhood of x st
for s being Real st |.(s - a).| < r holds
s * W c= V
let a be Real; :: thesis: for x being Point of X
for V being a_neighborhood of a * x ex r being positive Real ex W being a_neighborhood of x st
for s being Real st |.(s - a).| < r holds
s * W c= V
let x be Point of X; :: thesis: for V being a_neighborhood of a * x ex r being positive Real ex W being a_neighborhood of x st
for s being Real st |.(s - a).| < r holds
s * W c= V
let V be a_neighborhood of a * x; :: thesis: ex r being positive Real ex W being a_neighborhood of x st
for s being Real st |.(s - a).| < r holds
s * W c= V
a * x in Int V by CONNSP_2:def 1;
then consider r being positive Real, W being Subset of X such that
A1: W is open and
A2: x in W and
A3: for s being Real st |.(s - a).| < r holds
s * W c= Int V by Def9;
Int W = W by A1, TOPS_1:23;
then reconsider W = W as a_neighborhood of x by A2, CONNSP_2:def 1;
take r ; :: thesis: ex W being a_neighborhood of x st
for s being Real st |.(s - a).| < r holds
s * W c= V
take W ; :: thesis: for s being Real st |.(s - a).| < r holds
s * W c= V
let s be Real; :: thesis: ( |.(s - a).| < r implies s * W c= V )
assume |.(s - a).| < r ; :: thesis: s * W c= V
then A4: s * W c= Int V by A3;
Int V c= V by TOPS_1:16;
hence s * W c= V by A4; :: thesis: verum