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