{ N where N is a_neighborhood of A : verum } is Subset-Family of the carrier of ET

proof

{ N where N is a_neighborhood of A : verum } c= bool the carrier of ET

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { N where N is a_neighborhood of A : verum } or t in bool the carrier of ET )
assume t in { N where N is a_neighborhood of A : verum } ; :: thesis: t in bool the carrier of ET
then consider N0 being a_neighborhood of A such that
A1: t = N0 ;
thus t in bool the carrier of ET by A1; :: thesis: verum

end;

hence { N where N is a_neighborhood of A : verum } is Subset-Family of the carrier of ET ; :: thesis: verum

end;

hence { N where N is a_neighborhood of A : verum } is Subset-Family of ET ; :: thesis: verum