theorem Th72: :: ABCMIZ_1:72

for z being set
for C being initialized ConstructorSignature holds
( z is quasi-type of C iff ex A being finite Subset of (QuasiAdjs C) ex q being pure expression of C, a_Type C st z = [A,q] )