take TotFam T ; :: thesis: ( TotFam T is compl-closed & TotFam T is closed_for_countable_unions & TotFam T is closed_for_countable_meets & TotFam T is all-closed-containing & TotFam T is all-open-containing )
thus ( TotFam T is compl-closed & TotFam T is closed_for_countable_unions & TotFam T is closed_for_countable_meets & TotFam T is all-closed-containing & TotFam T is all-open-containing ) ; :: thesis: verum