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

proof

hence
{ N where N is open a_neighborhood of A : verum } is Subset-Family of the carrier of ET
; :: thesis: verum
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { N where N is open a_neighborhood of A : verum } or t in bool the carrier of ET )

assume t in { N where N is open a_neighborhood of A : verum } ; :: thesis: t in bool the carrier of ET

then consider N being open a_neighborhood of A such that

A1: t = N ;

thus t in bool the carrier of ET by A1; :: thesis: verum

end;assume t in { N where N is open a_neighborhood of A : verum } ; :: thesis: t in bool the carrier of ET

then consider N being open a_neighborhood of A such that

A1: t = N ;

thus t in bool the carrier of ET by A1; :: thesis: verum