let T be non empty TopSpace; :: thesis: for A being Subset of T st A is F_sigma holds

A ` is G_delta

let A be Subset of T; :: thesis: ( A is F_sigma implies A ` is G_delta )

assume A is F_sigma ; :: thesis: A ` is G_delta

then consider F being countable closed Subset-Family of T such that

A1: A = union F ;

A ` is G_delta

let A be Subset of T; :: thesis: ( A is F_sigma implies A ` is G_delta )

assume A is F_sigma ; :: thesis: A ` is G_delta

then consider F being countable closed Subset-Family of T such that

A1: A = union F ;