theorem :: ABCMIZ_A:48

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