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

A ` is F_sigma

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

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

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

A1: A = meet F ;

A ` is F_sigma

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

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

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

A1: A = meet F ;