consider G being Function of CQC-WFF,F₁() such that
A2: F₂(F₆()) = G . F₆() and
A3: ( G . VERUM = F₃() & ( for r, s being Element of CQC-WFF
for x being bound_QC-variable
for k being Element of NAT
for l being CQC-variable_list of k
for P being QC-pred_symbol of k holds
( G . (P ! l) = F₄(k,P,l) & G . ('not' r) = F₅((G . r)) & G . (r '&' s) = F₇((G . r),(G . s)) & G . (All (x,r)) = F₈(x,(G . r)) ) ) ) by A1;
consider F being Function of CQC-WFF,F₁() such that
A4: ( F . VERUM = F₃() & ( for r, s being Element of CQC-WFF
for x being bound_QC-variable
for k being Element of NAT
for l being CQC-variable_list of k
for P being QC-pred_symbol of k holds
( F . (P ! l) = F₄(k,P,l) & F . ('not' r) = F₅((F . r)) & F . (r '&' s) = F₇((F . r),(F . s)) & F . (All (x,r)) = F₈(x,(F . r)) ) ) ) from CQC_LANG:sch 2();
A5: F . ('not' F₆()) = F₅((F . F₆())) by A4;
F = G from CQC_LANG:sch 3(A4, A3);
hence F₂(('not' F₆())) = F₅(F₂(F₆())) by A1, A4, A5, A2; :: thesis: verum