let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al
for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st
( S `1 = p & S `2 = Sub )
defpred S₁[ Element of CQC-WFF Al] means for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st
( S `1 = $1 & S `2 = Sub );
A1: for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( S₁[ VERUM Al] & S₁[P ! ll] & ( S₁[p] implies S₁[ 'not' p] ) & ( S₁[p] & S₁[q] implies S₁[p '&' q] ) & ( S₁[p] implies S₁[ All (x,p)] ) ) by Th1, Th2, Th4, Th5, Th11;
thus for p being Element of CQC-WFF Al holds S₁[p] from CQC_LANG:sch 1(A1); :: thesis: verum