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

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