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

( F is open & {} T = meet F ) by Th19, SETFAM_1:10;

hence S is G_delta by A1; :: thesis: verum

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 F = {({} T)} as Subset-Family of T ;
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;{} T = union E by ZFMISC_1:2;

hence S is F_sigma by A1; :: thesis: verum

( F is open & {} T = meet F ) by Th19, SETFAM_1:10;

hence S is G_delta by A1; :: thesis: verum