let S be Subset of T; :: thesis: ( S is empty implies ( S is F_sigma & S is G_delta ) )
assume S is empty ; :: thesis: ( S is F_sigma & S is G_delta )
then X: S = {} T ;
thus S is F_sigma :: thesis: S is G_delta

proof

reconsider E = {} as empty Subset-Family of T by Th18;
{} T = union E by ZFMISC_1:2;
hence S is F_sigma by Def6, X; :: thesis: verum

end;

reconsider F = {({} T)} as Subset-Family of T ;
( F is open & {} T = meet F ) by Th19, SETFAM_1:11;
hence S is G_delta by Def7, X; :: thesis: verum