consider F being Function of CQC-WFF ,F₁() such that
A2: ( 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
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();
A3: F . ('not' F₆()) = F₅((F . F₆())) by A2;
consider G being Function of CQC-WFF ,F₁() such that
A4: F₂(F₆()) = G . F₆() and
A5: ( 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
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;
F = G from CQC_LANG:sch 3(A2, A5);
hence F₂(('not' F₆())) = F₅(F₂(F₆())) by A1, A2, A3, A4; :: thesis: verum