let T be non empty TopSpace; :: thesis: for p being Point of
for A being Element of holds A is a_neighborhood of p
let p be Point of ; :: thesis: for A being Element of holds A is a_neighborhood of p
let A be Element of ; :: thesis: A is a_neighborhood of p
ex W being Subset of st
( W = A & p in W & W is open ) by YELLOW_6:38;
hence A is a_neighborhood of p by CONNSP_2:5; :: thesis: verum