thus not TotFam T is empty ; :: thesis: ( TotFam T is all-open-containing & TotFam T is compl-closed & TotFam T is closed_for_countable_unions )
thus TotFam T is all-open-containing :: thesis: ( TotFam T is compl-closed & TotFam T is closed_for_countable_unions )

proof

let A be Subset of T; :: according to TOPGEN_4:def 2 :: thesis: ( A is open implies A in TotFam T )
assume A is open ; :: thesis: A in TotFam T
thus A in TotFam T ; :: thesis: verum

end;

for A being Subset of T st A in TotFam T holds
A ` in TotFam T ;
hence TotFam T is compl-closed by PROB_1:def 1; :: thesis: TotFam T is closed_for_countable_unions
for G being countable Subset-Family of T st G c= TotFam T holds
union G in TotFam T ;
hence TotFam T is closed_for_countable_unions by Def4; :: thesis: verum