let N be a_neighborhood of p; :: thesis: not N is empty
A1: p in Int N by CONNSP_2:def 1;
thus not N is empty by A1; :: thesis: verum