consider D being non trivial set ;
take ADTS D ; :: thesis: ( ADTS D is anti-discrete & not ADTS D is trivial & not ADTS D is empty & ADTS D is strict )
thus ( ADTS D is anti-discrete & not ADTS D is trivial & not ADTS D is empty & ADTS D is strict ) ; :: thesis: verum