consider IT being Subset of such that
A1: for p being Point of holds
( p in IT iff S₁[p] ) from SUBSET_1:sch 3();
take IT ; :: thesis: for p being Point of holds
( p in IT iff for V being a_neighborhood of p holds N is_eventually_in V )
let p be Point of ; :: 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