A6: for r, s being Element of CQC-WFF
for x being Element of bound_QC-variables
for k being Element of NAT
for l being CQC-variable_list of k
for P being QC-pred_symbol of k holds
( P₁[ VERUM ] & 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 holds P₁[r] from CQC_LANG:sch 1(A6); :: thesis: verum