let T be non empty TopSpace; :: thesis: for p being Point of T
for A being Element of (OpenNeighborhoods p) holds A is a_neighborhood of p
let p be Point of T; :: thesis: for A being Element of (OpenNeighborhoods p) holds A is a_neighborhood of p
let A be Element of (OpenNeighborhoods p); :: thesis: A is a_neighborhood of p
consider W being Subset of T such that
A1: ( W = A & p in W & W is open ) by YELLOW_6:38;
thus A is a_neighborhood of p by A1, CONNSP_2:5; :: thesis: verum