deffunc H₅( Nat, QC-pred_symbol of $1,A, CQC-variable_list of $1,A) -> Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) = ATOMIC ($2,$3);
set D = [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):];
deffunc H₆( Function of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A), set ) -> Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) = NEGATIVE $1;
deffunc H₇( Function of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A), Function of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A), Element of CQC-WFF A, set ) -> Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) = CON ($1,$2,(QuantNbr $3));
deffunc H₈( Element of bound_QC-variables A, Function of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A), set ) -> Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) = UNIVERSAL ($1,$2);
reconsider V = [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] --> (VERUM A) as Function of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A) ;
reconsider V = V as Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) by FUNCT_2:8;
consider F being Function of (CQC-WFF A),(Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A))) such that
A1: F . (VERUM A) = V and
A2: for k being Nat
for l being CQC-variable_list of k,A
for P being QC-pred_symbol of k,A holds F . (P ! l) = H₅(k,P,l) and
A3: for r, s being Element of CQC-WFF A
for x being Element of bound_QC-variables A holds
( F . ('not' r) = H₆(F . r,r) & F . (r '&' s) = H₇(F . r,F . s,r,s) & F . (All (x,r)) = H₈(x,F . r,r) ) from CQC_SIM1:sch 2();
take F ; :: thesis: ( F . (VERUM A) = [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] --> (VERUM A) & ( for k being Nat
for l being CQC-variable_list of k,A
for P being QC-pred_symbol of k,A holds F . (P ! l) = ATOMIC (P,l) ) & ( for r, s being Element of CQC-WFF A
for x being Element of bound_QC-variables A holds
( F . ('not' r) = NEGATIVE (F . r) & F . (r '&' s) = CON ((F . r),(F . s),(QuantNbr r)) & F . (All (x,r)) = UNIVERSAL (x,(F . r)) ) ) )
thus ( F . (VERUM A) = [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] --> (VERUM A) & ( for k being Nat
for l being CQC-variable_list of k,A
for P being QC-pred_symbol of k,A holds F . (P ! l) = ATOMIC (P,l) ) & ( for r, s being Element of CQC-WFF A
for x being Element of bound_QC-variables A holds
( F . ('not' r) = NEGATIVE (F . r) & F . (r '&' s) = CON ((F . r),(F . s),(QuantNbr r)) & F . (All (x,r)) = UNIVERSAL (x,(F . r)) ) ) ) by A1, A2, A3; :: thesis: verum