defpred S₁[ set ] means F₃() . $1 = F₄() . $1;
A3: 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
( S₁[ VERUM F₁()] & S₁[P ! l] & ( 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 bound_QC-variable of F₁(); :: thesis:
let k be Nat; :: thesis:
let l 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, A2; :: thesis:
F₃() . (P ! l) = F₆(k,P,l) by A1;
hence F₃() . (P ! l) = F₄() . (P ! l) by A2; :: thesis:
F₃() . ('not' r) = F₇((F₃() . r)) by A1;
hence ( F₃() . r = F₄() . r implies F₃() . ('not' r) = F₄() . ('not' r) ) by A2; :: thesis:
F₃() . (r '&' s) = F₈((F₃() . r),(F₃() . s)) by A1;
hence ( F₃() . r = F₄() . r & F₃() . s = F₄() . s implies F₃() . (r '&' s) = F₄() . (r '&' s) ) by A2; :: thesis:
F₃() . (All (x,r)) = F₉(x,(F₃() . r)) by A1;
hence ( S₁[r] implies S₁[ All (x,r)] ) by A2; :: thesis:

end;