let it1, it2 be Subset of T; :: thesis: ( ( for p being Point of T holds
( p in it1 iff for V being a_neighborhood of p holds N is_eventually_in V ) ) & ( for p being Point of T holds
( p in it2 iff for V being a_neighborhood of p holds N is_eventually_in V ) ) implies it1 = it2 )
assume that
A2: for p being Point of T holds
( p in it1 iff S₁[p] ) and
A3: for p being Point of T holds
( p in it2 iff S₁[p] ) ; :: thesis: it1 = it2
thus it1 = it2 from SUBSET_1:sch 4(A2, A3); :: thesis: verum