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