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

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