defpred S₁[ Point of ] means for G being a_neighborhood of $1 ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets G;
thus ex IT being Subset of st
for p being Point of holds
( p in IT iff S₁[p] ) from SUBSET_1:sch 3(); :: thesis: verum