ex F being Function of CQC-WFF,F₁() st
( 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();
hence F₂(VERUM) = F₃() by A1; :: thesis: verum