A6: for r, s being Element of CQC-WFF F₁()
for x being bound_QC-variable of F₁()
for k being Nat
for l being CQC-variable_list of k,F₁()
for P being QC-pred_symbol of k,F₁() holds
( P₁[ VERUM F₁()] & P₁[P ! l] & ( P₁[r] implies P₁[ 'not' r] ) & ( P₁[r] & P₁[s] implies P₁[r '&' s] ) & ( P₁[r] implies P₁[ All (x,r)] ) ) by A1, A2, A3, A4, A5;
thus for r being Element of CQC-WFF F₁() holds P₁[r] from CQC_LANG:sch 1(A6); :: thesis: verum