consider IT being Subset of T such that
A1: for p being Point of T holds
( p in IT iff S₁[p] ) from SUBSET_1:sch 3();
take IT ; :: thesis: for p being Point of T holds
( p in IT iff for V being a_neighborhood of p holds N is_eventually_in V )
let p be Point of T; :: thesis: ( p in IT iff for V being a_neighborhood of p holds N is_eventually_in V )
thus ( p in IT iff for V being a_neighborhood of p holds N is_eventually_in V ) by A1; :: thesis: verum