let X be NormedLinearTopSpace; :: thesis: for V being Subset of X
for x being Point of X holds
( V is a_neighborhood of x iff ex r being Real st
( r > 0 & { y where y is Point of X : ||.(y - x).|| < r } c= V ) )
let V be Subset of X; :: thesis: for x being Point of X holds
( V is a_neighborhood of x iff ex r being Real st
( r > 0 & { y where y is Point of X : ||.(y - x).|| < r } c= V ) )
let x be Point of X; :: thesis: ( V is a_neighborhood of x iff ex r being Real st
( r > 0 & { y where y is Point of X : ||.(y - x).|| < r } c= V ) )
hereby :: thesis: ( ex r being Real st
( r > 0 & { y where y is Point of X : ||.(y - x).|| < r } c= V ) implies V is a_neighborhood of x )
assume V is a_neighborhood of x ; :: thesis: ex r being Real st
( r > 0 & { y where y is Point of X : ||.(y - x).|| < r } c= V )
then consider U being Subset of X such that
A1: U is open and
A2: U c= V and
A3: x in U by CONNSP_2:6;
consider r being Real such that
A4: ( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= U ) by Th23, A1, A3;
{ y where y is Point of X : ||.(x - y).|| < r } = { y where y is Point of X : ||.(y - x).|| < r } by Lm1;
hence ex r being Real st
( r > 0 & { y where y is Point of X : ||.(y - x).|| < r } c= V ) by A4, A2, XBOOLE_1:1; :: thesis: verum
end;
given r being Real such that A5: ( r > 0 & { y where y is Point of X : ||.(y - x).|| < r } c= V ) ; :: thesis: V is a_neighborhood of x
reconsider U = { y where y is Point of X : ||.(y - x).|| < r } as Subset of X by A5, XBOOLE_1:1;
A6: { y where y is Point of X : ||.(y - x).|| < r } = { y where y is Point of X : ||.(x - y).|| < r } by Lm1;
||.(x - x).|| = 0 by NORMSP_1:6;
then x in U by A5;
hence V is a_neighborhood of x by A5, A6, Th24, CONNSP_2:6; :: thesis: verum