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