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

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