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 ;
per cases ( F <> {} or F = {} ) ;
suppose A2: F <> {} ; :: thesis: A ` is G_delta
set G = COMPLEMENT F;
A3: COMPLEMENT F is open by TOPS_2:9;
(union F) ` = meet (COMPLEMENT F) by A2, TOPS_2:6;
hence A ` is G_delta by A1, A3; :: thesis: verum
end;
suppose F = {} ; :: thesis: A ` is G_delta
then A ` = [#] T by A1, ZFMISC_1:2;
hence A ` is G_delta ; :: thesis: verum
end;
end;