set Z = { x where x is Point of T : F is_filter-finer_than NeighborhoodSystem x } ;

now :: thesis: for x being object st x in { x where x is Point of T : F is_filter-finer_than NeighborhoodSystem x } holds
x in the carrier of T

let x be object ; :: thesis: ( x in { x where x is Point of T : F is_filter-finer_than NeighborhoodSystem x } implies x in the carrier of T )
assume x in { x where x is Point of T : F is_filter-finer_than NeighborhoodSystem x } ; :: thesis: x in the carrier of T
then consider x0 being Point of T such that
A1: x = x0 and
F is_filter-finer_than NeighborhoodSystem x0 ;
thus x in the carrier of T by A1; :: thesis: verum

end;

then { x where x is Point of T : F is_filter-finer_than NeighborhoodSystem x } c= the carrier of T ;
hence { x where x is Point of T : F is_filter-finer_than NeighborhoodSystem x } is Subset of T ; :: thesis: verum