set SN = { (Neighborhood (V,x)) where V is Element of the entourages of USS : verum } ;
{ (Neighborhood (V,x)) where V is Element of the entourages of USS : verum } c= bool the carrier of USS

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { (Neighborhood (V,x)) where V is Element of the entourages of USS : verum } or t in bool the carrier of USS )
assume t in { (Neighborhood (V,x)) where V is Element of the entourages of USS : verum } ; :: thesis: t in bool the carrier of USS
then ex V being Element of the entourages of USS st t = Neighborhood (V,x) ;
hence t in bool the carrier of USS ; :: thesis: verum

end;

hence { (Neighborhood (V,x)) where V is Element of the entourages of USS : verum } is Subset-Family of USS ; :: thesis: verum