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

set X = the carrier of T;

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

proof

hence
{ A where A is a_neighborhood of x : verum } is Subset of (BoolePoset ([#] T))
by WAYBEL_7:2; :: thesis: verum
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;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