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

proof

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

end;proof

hence
{ N where N is 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 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;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