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