theorem :: ABCMIZ_1:82

for C being initialized ConstructorSignature
for T being quasi-type of C
for a being quasi-adjective of C holds
( adjs (a ast T) = {a} \/ (adjs T) & the_base_of (a ast T) = the_base_of T ) ;