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 A1: 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 A1; :: thesis: verum
end;
reconsider F = {({} T)} as Subset-Family of T ;
( F is open & {} T = meet F ) by Th19, SETFAM_1:10;
hence S is G_delta by A1; :: thesis: verum