let T be non empty TopSpace; :: thesis: for A being Subset of T st A is closed holds
A is F_sigma
let A be Subset of T; :: thesis: ( A is closed implies A is F_sigma )
assume A is closed ; :: thesis: A is F_sigma
then reconsider F = {A} as countable closed Subset-Family of T by Th20;
take F ; :: according to TOPGEN_4:def 6 :: thesis: A = union F
thus A = union F by ZFMISC_1:25; :: thesis: verum