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;
let a, b be Subset of T; :: thesis: ( ( for p being Point of T holds
( p in a iff for G being a_neighborhood of p ex k being Nat st
for m being Nat st m > k holds
S . m meets G ) ) & ( for p being Point of T holds
( p in b iff for G being a_neighborhood of p ex k being Nat st
for m being Nat st m > k holds
S . m meets G ) ) implies a = b )
assume that
A1: for p being Point of T holds
( p in a iff S₁[p] ) and
A2: for p being Point of T holds
( p in b iff S₁[p] ) ; :: thesis: a = b
thus a = b from SUBSET_1:sch 2(A1, A2); :: thesis: verum