let T be non empty TopSpace; :: thesis: ( sigma (TotFam T) is all-open-containing & sigma (TotFam T) is compl-closed & sigma (TotFam T) is closed_for_countable_unions )
set E = sigma (TotFam T);
TotFam T c= sigma (TotFam T) by PROB_1:def 9;
hence sigma (TotFam T) is all-open-containing ; :: thesis: ( sigma (TotFam T) is compl-closed & sigma (TotFam T) is closed_for_countable_unions )
thus sigma (TotFam T) is compl-closed ; :: thesis: sigma (TotFam T) is closed_for_countable_unions
thus sigma (TotFam T) is closed_for_countable_unions ; :: thesis: verum