reconsider B = [#] T as a_neighborhood of p by Th20;
take B ; :: thesis: ( not B is empty & B is open )
thus ( not B is empty & B is open ) ; :: thesis: verum