take sigma (TotFam T) ; :: thesis: sigma (TotFam T) is all-open-containing
thus sigma (TotFam T) is all-open-containing ; :: thesis: verum