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

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