set Y = { A where A is a_neighborhood of x : verum } ;
set X = the carrier of T;
{ A where A is a_neighborhood of x : verum } c= bool the carrier of T

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { A where A is a_neighborhood of x : verum } or y in bool the carrier of T )
assume y in { A where A is a_neighborhood of x : verum } ; :: thesis: y in bool the carrier of T
then ex A being a_neighborhood of x st y = A ;
hence y in bool the carrier of T ; :: thesis: verum

end;

hence { A where A is a_neighborhood of x : verum } is Subset of (BoolePoset ([#] T)) by WAYBEL_7:2; :: thesis: verum