set S = { x where x is Point of NT : x is_adherent_point_of A } ;
{ x where x is Point of NT : x is_adherent_point_of A } c= the carrier of NT

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in { x where x is Point of NT : x is_adherent_point_of A } or o in the carrier of NT )
assume o in { x where x is Point of NT : x is_adherent_point_of A } ; :: thesis: o in the carrier of NT
then ex x being Point of NT st
( o = x & x is_adherent_point_of A ) ;
hence o in the carrier of NT ; :: thesis: verum

end;

hence { x where x is Point of NT : x is_adherent_point_of A } is Subset of NT ; :: thesis: verum