deffunc H₁( Element of NAT , QC-pred_symbol of $1, CQC-variable_list of $1) -> Element of Funcs ((Valuations_in A),BOOLEAN) = $3 'in' (J . $2);
set V = (Valuations_in A) --> TRUE;
set D = Funcs ((Valuations_in A),BOOLEAN);
deffunc H₂( Element of Funcs ((Valuations_in A),BOOLEAN)) -> Element of Funcs ((Valuations_in A),BOOLEAN) = 'not' $1;
deffunc H₃( Element of Funcs ((Valuations_in A),BOOLEAN), Element of Funcs ((Valuations_in A),BOOLEAN)) -> Element of Funcs ((Valuations_in A),BOOLEAN) = $1 '&' $2;
deffunc H₄( bound_QC-variable, Element of Funcs ((Valuations_in A),BOOLEAN)) -> Element of Funcs ((Valuations_in A),BOOLEAN) = FOR_ALL ($1,$2);
thus ( ex d being Element of Funcs ((Valuations_in A),BOOLEAN) ex F being Function of CQC-WFF,(Funcs ((Valuations_in A),BOOLEAN)) st
( d = F . p & F . VERUM = (Valuations_in A) --> TRUE & ( 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) = H₁(k,P,l) & F . ('not' r) = H₂(F . r) & F . (r '&' s) = H₃(F . r,F . s) & F . (All (x,r)) = H₄(x,F . r) ) ) ) & ( for d1, d2 being Element of Funcs ((Valuations_in A),BOOLEAN) st ex F being Function of CQC-WFF,(Funcs ((Valuations_in A),BOOLEAN)) st
( d1 = F . p & F . VERUM = (Valuations_in A) --> TRUE & ( 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) = H₁(k,P,l) & F . ('not' r) = H₂(F . r) & F . (r '&' s) = H₃(F . r,F . s) & F . (All (x,r)) = H₄(x,F . r) ) ) ) & ex F being Function of CQC-WFF,(Funcs ((Valuations_in A),BOOLEAN)) st
( d2 = F . p & F . VERUM = (Valuations_in A) --> TRUE & ( 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) = H₁(k,P,l) & F . ('not' r) = H₂(F . r) & F . (r '&' s) = H₃(F . r,F . s) & F . (All (x,r)) = H₄(x,F . r) ) ) ) holds
d1 = d2 ) ) from CQC_LANG:sch 4(); :: thesis: verum