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

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, Th25;
A is closed by A1, Th25;
hence A is nowhere_dense by A2; :: thesis: verum

end;

hence not STS C,c0 is almost_discrete by Def7; :: 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 by Def7;
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:39;
hence contradiction by A3, TOPS_3:23; :: thesis: verum