let q be pure expression of MaxConstrSign , a_Type MaxConstrSign; :: thesis: 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 } )
let A be finite Subset of (QuasiAdjs MaxConstrSign); :: thesis: constrs (A ast q) = (constrs q) \/ (union { (constrs a) where a is quasi-adjective : a in A } )
set T = A ast q;
A1: A = adjs (A ast q) by ABCMIZ_1:78;
thus constrs (A ast q) = (constrs (the_base_of (A ast q))) \/ (union { (constrs a) where a is quasi-adjective : a in adjs (A ast q) } )
.= (constrs q) \/ (union { (constrs a) where a is quasi-adjective : a in A } ) by A1, ABCMIZ_1:78 ; :: thesis: verum