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

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