let C be non empty set ; :: thesis: for c0 being Element of C holds
( not C \ {c0} is empty iff not STS (C,c0) is almost_discrete )
let c0 be Element of C; :: thesis: ( not C \ {c0} is empty iff not STS (C,c0) is almost_discrete )

hereby :: thesis: ( not STS (C,c0) is almost_discrete implies not C \ {c0} is empty )

assume A1: not C \ {c0} is empty ; :: thesis: not STS (C,c0) is almost_discrete

now :: thesis: ex A being non empty Subset of (STS (C,c0)) st A is nowhere_dense

reconsider A = {c0} as non empty Subset of (STS (C,c0)) ;
take A = A; :: thesis: A is nowhere_dense
A2: A is boundary by A1, Th21;
A is closed by A1, Th21;
hence A is nowhere_dense by A2; :: thesis: verum

end;

hence not STS (C,c0) is almost_discrete ; :: thesis: verum

end;

assume not STS (C,c0) is almost_discrete ; :: thesis: not C \ {c0} is empty
then consider A being non empty Subset of (STS (C,c0)) such that
A3: A is nowhere_dense ;
assume C \ {c0} is empty ; :: thesis: contradiction
then C c= {c0} by XBOOLE_1:37;
then C = {c0} by XBOOLE_0:def 10;
then A = C by ZFMISC_1:33;
hence contradiction by A3, TOPS_3:23; :: thesis: verum