theorem Th80: :: ABCMIZ_1:80

for C being initialized ConstructorSignature
for T being quasi-type of C holds T = (adjs T) ast (the_base_of T) ;