deffunc H₅( Element of NAT , QC-pred_symbol of $1, CQC-variable_list of $1) -> Element of Funcs ([:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):],CQC-WFF) = ATOMIC ($2,$3);
set D = [:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):];
deffunc H₆( Function of [:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):],CQC-WFF, set ) -> Element of Funcs ([:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):],CQC-WFF) = NEGATIVE $1;
deffunc H₇( Function of [:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):],CQC-WFF, Function of [:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):],CQC-WFF, Element of CQC-WFF , set ) -> Element of Funcs ([:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):],CQC-WFF) = CON ($1,$2,(QuantNbr $3));
deffunc H₈( Element of bound_QC-variables , Function of [:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):],CQC-WFF, set ) -> Element of Funcs ([:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):],CQC-WFF) = UNIVERSAL ($1,$2);
reconsider V = [:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):] --> VERUM as Function of [:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):],CQC-WFF ;
reconsider V = V as Element of Funcs ([:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):],CQC-WFF) by FUNCT_2:11;
consider F being Function of CQC-WFF,(Funcs ([:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):],CQC-WFF)) such that
A1: F . VERUM = V and
A2: 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) = H₅(k,P,l) and
A3: for r, s being Element of CQC-WFF
for x being Element of bound_QC-variables 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 = [:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):] --> VERUM & ( 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) = ATOMIC (P,l) ) & ( for r, s being Element of CQC-WFF
for x being Element of bound_QC-variables 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 = [:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):] --> VERUM & ( 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) = ATOMIC (P,l) ) & ( for r, s being Element of CQC-WFF
for x being Element of bound_QC-variables 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