:: deftheorem defines constrs ABCMIZ_A:def 20 :
for T being quasi-type holds constrs T = (constrs (the_base_of T)) \/ (union { (constrs a) where a is quasi-adjective : a in adjs T } );