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:37;
then reconsider f = NAT --> {the carrier of T} as Function of NAT , bool (bool the carrier of T) by FUNCOP_1:57;
take f ; :: thesis: f is sigma_discrete

now

let n be Element of NAT ; :: thesis: f . n is discrete
the carrier of T is Subset of by ZFMISC_1:def 1;
hence f . n is discrete by Th1, FUNCOP_1:13; :: thesis: verum

end;

hence f is sigma_discrete by Def2; :: thesis: verum