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 ;

per cases ( F <> {} or F = {} ) ;

suppose A2: F <> {} ; :: thesis: A ` is F_sigma

set G = COMPLEMENT F;
A3: COMPLEMENT F is closed by TOPS_2:10;
(meet F) ` = union (COMPLEMENT F) by A2, TOPS_2:7;
hence A ` is F_sigma by A1, A3; :: thesis: verum

end;

suppose F = {} ; :: thesis: A ` is F_sigma

then A ` = [#] T by A1, SETFAM_1:1;
hence A ` is F_sigma ; :: thesis: verum

end;

end;