set S = { x where x is Point of NTX : F is_filter-finer_than U_FMT x } ;

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

let x be object ; :: thesis: ( x in { x where x is Point of NTX : F is_filter-finer_than U_FMT x } implies x in the carrier of NTX )
assume x in { x where x is Point of NTX : F is_filter-finer_than U_FMT x } ; :: thesis: x in the carrier of NTX
then ex y being Point of NTX st
( x = y & F is_filter-finer_than U_FMT y ) ;
hence x in the carrier of NTX ; :: thesis: verum

end;

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