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 ) )

A2: now

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

end;

now

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

end;

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