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: for i being Nat holds S . i is closed by FUNCOP_1:7, ORDINAL1:def 12;
for i being Nat holds S . i is open by FUNCOP_1:7, ORDINAL1:def 12;
hence ( S is open & S is closed ) by A1; :: thesis: ( not T is empty implies S is non-empty )
assume not T is empty ; :: thesis: S is non-empty
then for x being object 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