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

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