let T be non empty TopSpace; :: thesis: ( not T is anti-discrete implies not T is trivial )
assume not T is anti-discrete ; :: thesis: not T is trivial
then T is not 1 -element TopSpace ;
then not the carrier of T is 1 -element by STRUCT_0:def 19;
hence not T is trivial ; :: thesis: verum