ADTS D = TopStruct(# D,(cobool D) #) by TEX_1:def 3;
hence not ADTS D is trivial ; :: thesis: verum