defpred S₁[ set ] means F₄() . $1 = F₅() . $1;
A7: for r, s being Element of CQC-WFF F₁()
for x being bound_QC-variable of F₁()
for k being Nat
for ll being CQC-variable_list of k,F₁()
for P being QC-pred_symbol of k,F₁() holds
( S₁[ VERUM F₁()] & S₁[P ! ll] & ( S₁[r] implies S₁[ 'not' r] ) & ( S₁[r] & S₁[s] implies S₁[r '&' s] ) & ( S₁[r] implies S₁[ All (x,r)] ) )

let r, s be Element of CQC-WFF F₁(); :: thesis:
let x be Element of bound_QC-variables F₁(); :: thesis:
let k be Nat; :: thesis:
let ll be CQC-variable_list of k,F₁(); :: thesis:
let P be QC-pred_symbol of k,F₁(); :: thesis:
thus F₄() . (VERUM F₁()) = F₅() . (VERUM F₁()) by A1, A4; :: thesis:
reconsider k = k as Element of NAT by ORDINAL1:def 12;
reconsider l1 = ll as CQC-variable_list of k,F₁() ;
F₄() . (P ! l1) = F₇(k,P,l1) by A2;
hence F₄() . (P ! ll) = F₅() . (P ! ll) by A5; :: thesis:
F₄() . ('not' r) = F₈((F₄() . r),r) by A3;
hence ( F₄() . r = F₅() . r implies F₄() . ('not' r) = F₅() . ('not' r) ) by A6; :: thesis:
F₄() . (r '&' s) = F₉((F₄() . r),(F₄() . s),r,s) by A3;
hence ( F₄() . r = F₅() . r & F₄() . s = F₅() . s implies F₄() . (r '&' s) = F₅() . (r '&' s) ) by A6; :: thesis:
F₄() . (All (x,r)) = F₁₀(x,(F₄() . r),r) by A3;
hence ( S₁[r] implies S₁[ All (x,r)] ) by A6; :: thesis:

end;