let T be non empty TopSpace; :: thesis: for x being Point of T
for A being set holds
( A in NeighborhoodSystem x iff A is a_neighborhood of x )
let x be Point of T; :: thesis: for A being set holds
( A in NeighborhoodSystem x iff A is a_neighborhood of x )
let B be set ; :: thesis: ( B in NeighborhoodSystem x iff B is a_neighborhood of x )
( B in NeighborhoodSystem x iff ex A being a_neighborhood of x st B = A ) ;
hence ( B in NeighborhoodSystem x iff B is a_neighborhood of x ) ; :: thesis: verum