let X be non empty TopSpace; :: thesis: for x being Point of X

for V being Subset of X holds

( V is a_neighborhood of {x} iff V is a_neighborhood of x )

let x be Point of X; :: thesis: for V being Subset of X holds

( V is a_neighborhood of {x} iff V is a_neighborhood of x )

let V be Subset of X; :: thesis: ( V is a_neighborhood of {x} iff V is a_neighborhood of x )

thus ( V is a_neighborhood of {x} implies V is a_neighborhood of x ) :: thesis: ( V is a_neighborhood of x implies V is a_neighborhood of {x} )

then x in Int V by Def1;

then for p being object st p in {x} holds

p in Int V by TARSKI:def 1;

then {x} c= Int V ;

hence V is a_neighborhood of {x} by Def2; :: thesis: verum

for V being Subset of X holds

( V is a_neighborhood of {x} iff V is a_neighborhood of x )

let x be Point of X; :: thesis: for V being Subset of X holds

( V is a_neighborhood of {x} iff V is a_neighborhood of x )

let V be Subset of X; :: thesis: ( V is a_neighborhood of {x} iff V is a_neighborhood of x )

thus ( V is a_neighborhood of {x} implies V is a_neighborhood of x ) :: thesis: ( V is a_neighborhood of x implies V is a_neighborhood of {x} )

proof

assume
V is a_neighborhood of x
; :: thesis: V is a_neighborhood of {x}
assume
V is a_neighborhood of {x}
; :: thesis: V is a_neighborhood of x

then A1: {x} c= Int V by Def2;

x in {x} by TARSKI:def 1;

hence V is a_neighborhood of x by A1, Def1; :: thesis: verum

end;then A1: {x} c= Int V by Def2;

x in {x} by TARSKI:def 1;

hence V is a_neighborhood of x by A1, Def1; :: thesis: verum

then x in Int V by Def1;

then for p being object st p in {x} holds

p in Int V by TARSKI:def 1;

then {x} c= Int V ;

hence V is a_neighborhood of {x} by Def2; :: thesis: verum