let T be TopSpace; :: thesis: ex S being SetSequence of T st
( S is open & S is closed & ( not T is empty implies S is non-empty ) )
take S = NAT --> ([#] T); :: thesis: ( S is open & S is closed & ( not T is empty implies S is non-empty ) )

A1: now

let i be natural number ; :: thesis: S . i is closed
i in NAT by ORDINAL1:def 12;
hence S . i is closed by FUNCOP_1:7; :: thesis: verum

end;

now

let i be natural number ; :: thesis: S . i is open
i in NAT by ORDINAL1:def 12;
hence S . i is open by FUNCOP_1:7; :: thesis: verum

end;

hence ( S is open & S is closed ) by A1, Def5, Def6; :: thesis: ( not T is empty implies S is non-empty )
assume not T is empty ; :: thesis: S is non-empty
then for x being set st x in dom S holds
not S . x is empty by FUNCOP_1:7;
hence S is non-empty by FUNCT_1:def 9; :: thesis: verum