theorem :: ABCMIZ_1:105

for C being initialized ConstructorSignature
for q being pure expression of C, a_Type C
for A being finite Subset of (QuasiAdjs C) holds vars (A ast q) = (union { (vars a) where a is quasi-adjective of C : a in A } ) \/ (vars q)