take E = sigma (TotFam T); :: thesis: ( E is sigma-additive & E is compl-closed & E is closed_for_countable_unions & not E is empty )
thus ( E is sigma-additive & E is compl-closed & E is closed_for_countable_unions & not E is empty ) ; :: thesis: verum