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