theorem :: ABCMIZ_1:78

for C being initialized ConstructorSignature
for q being pure expression of C, a_Type C
for A being finite Subset of (QuasiAdjs C) holds
( adjs (A ast q) = A & the_base_of (A ast q) = q ) ;