let T be non empty TopSpace; :: thesis: for Un being FamilySequence of T st Un is sigma_discrete holds
Un is sigma_locally_finite
let Un be FamilySequence of T; :: thesis: ( Un is sigma_discrete implies Un is sigma_locally_finite )
assume A1: Un is sigma_discrete ; :: thesis: Un is sigma_locally_finite
let n be Element of NAT ; :: according to NAGATA_1:def 3 :: thesis: Un . n is locally_finite
Un . n is discrete by A1, Def2;
hence Un . n is locally_finite by Th11; :: thesis: verum