let T be non empty TopSpace; :: thesis: ex Un being FamilySequence of T st Un is sigma_discrete
set C = { the carrier of T};
the carrier of T in bool the carrier of T by ZFMISC_1:def 1;
then { the carrier of T} c= bool the carrier of T by ZFMISC_1:31;
then reconsider f = NAT --> { the carrier of T} as sequence of (bool (bool the carrier of T)) by FUNCOP_1:45;
take f ; :: thesis: f is sigma_discrete
now :: thesis: for n being Element of NAT holds f . n is discrete
let n be Element of NAT ; :: thesis: f . n is discrete
the carrier of T is Subset of T by ZFMISC_1:def 1;
hence f . n is discrete by Th1, FUNCOP_1:7; :: thesis: verum
end;
hence f is sigma_discrete ; :: thesis: verum