let T be non empty TopSpace; :: thesis: for p being Point of T holds [#] T is a_neighborhood of p
let p be Point of T; :: thesis: [#] T is a_neighborhood of p
Int ([#] T) = the carrier of T by TOPS_1:15;
hence p in Int ([#] T) ; :: according to CONNSP_2:def 1 :: thesis: verum