let p be Element of CQC-WFF ; :: thesis: for A being non empty set
for J being interpretation of A holds
( Valid VERUM ,J = (Valuations_in A) --> TRUE & ( for k being Element of NAT
for ll being CQC-variable_list of k
for P being QC-pred_symbol of k holds Valid (P ! ll),J = ll 'in' (J . P) ) & ( for p being Element of CQC-WFF holds Valid ('not' p),J = 'not' (Valid p,J) ) & ( for q being Element of CQC-WFF holds Valid (p '&' q),J = (Valid p,J) '&' (Valid q,J) ) & ( for x being bound_QC-variable holds Valid (All x,p),J = FOR_ALL x,(Valid p,J) ) )
let A be non empty set ; :: thesis: for J being interpretation of A holds
( Valid VERUM ,J = (Valuations_in A) --> TRUE & ( for k being Element of NAT
for ll being CQC-variable_list of k
for P being QC-pred_symbol of k holds Valid (P ! ll),J = ll 'in' (J . P) ) & ( for p being Element of CQC-WFF holds Valid ('not' p),J = 'not' (Valid p,J) ) & ( for q being Element of CQC-WFF holds Valid (p '&' q),J = (Valid p,J) '&' (Valid q,J) ) & ( for x being bound_QC-variable holds Valid (All x,p),J = FOR_ALL x,(Valid p,J) ) )
let J be interpretation of A; :: thesis: ( Valid VERUM ,J = (Valuations_in A) --> TRUE & ( for k being Element of NAT
for ll being CQC-variable_list of k
for P being QC-pred_symbol of k holds Valid (P ! ll),J = ll 'in' (J . P) ) & ( for p being Element of CQC-WFF holds Valid ('not' p),J = 'not' (Valid p,J) ) & ( for q being Element of CQC-WFF holds Valid (p '&' q),J = (Valid p,J) '&' (Valid q,J) ) & ( for x being bound_QC-variable holds Valid (All x,p),J = FOR_ALL x,(Valid p,J) ) )
set D = Funcs (Valuations_in A),BOOLEAN ;
set V = (Valuations_in A) --> TRUE ;
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);
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;
deffunc H₅( Element of CQC-WFF ) -> Element of Funcs (Valuations_in A),BOOLEAN = Valid $1,J;
A1: for p being Element of CQC-WFF
for d being Element of Funcs (Valuations_in A),BOOLEAN holds
( d = H₅(p) iff ex F being Function of CQC-WFF ,(Funcs (Valuations_in A),BOOLEAN ) st
( d = F . p & F . VERUM = (Valuations_in A) --> TRUE & ( for p, q being Element of CQC-WFF
for x being bound_QC-variable
for k being Element of NAT
for ll being CQC-variable_list of k
for P being QC-pred_symbol of k holds
( F . (P ! ll) = H₁(k,P,ll) & F . ('not' p) = H₂(F . p) & F . (p '&' q) = H₃(F . p,F . q) & F . (All x,p) = H₄(x,F . p) ) ) ) ) by Def11;
thus H₅( VERUM ) = (Valuations_in A) --> TRUE from CQC_LANG:sch 5(A1); :: thesis: ( ( for k being Element of NAT
for ll being CQC-variable_list of k
for P being QC-pred_symbol of k holds Valid (P ! ll),J = ll 'in' (J . P) ) & ( for p being Element of CQC-WFF holds Valid ('not' p),J = 'not' (Valid p,J) ) & ( for q being Element of CQC-WFF holds Valid (p '&' q),J = (Valid p,J) '&' (Valid q,J) ) & ( for x being bound_QC-variable holds Valid (All x,p),J = FOR_ALL x,(Valid p,J) ) )

hereby :: thesis: ( ( for p being Element of CQC-WFF holds Valid ('not' p),J = 'not' (Valid p,J) ) & ( for q being Element of CQC-WFF holds Valid (p '&' q),J = (Valid p,J) '&' (Valid q,J) ) & ( for x being bound_QC-variable holds Valid (All x,p),J = FOR_ALL x,(Valid p,J) ) )

let k be Element of NAT ; :: thesis: for ll being CQC-variable_list of k
for P being QC-pred_symbol of k holds H₅(P ! ll) = H₁(k,P,ll)
let ll be CQC-variable_list of k; :: thesis: for P being QC-pred_symbol of k holds H₅(P ! ll) = H₁(k,P,ll)
let P be QC-pred_symbol of k; :: thesis: H₅(P ! ll) = H₁(k,P,ll)
thus H₅(P ! ll) = H₁(k,P,ll) from CQC_LANG:sch 6(A1); :: thesis: verum

end;

hereby :: thesis: ( ( for q being Element of CQC-WFF holds Valid (p '&' q),J = (Valid p,J) '&' (Valid q,J) ) & ( for x being bound_QC-variable holds Valid (All x,p),J = FOR_ALL x,(Valid p,J) ) )

let p be Element of CQC-WFF ; :: thesis: H₅( 'not' p) = H₂(H₅(p))
thus H₅( 'not' p) = H₂(H₅(p)) from CQC_LANG:sch 7(A1); :: thesis: verum

end;

hereby :: thesis: for x being bound_QC-variable holds Valid (All x,p),J = FOR_ALL x,(Valid p,J)

let q be Element of CQC-WFF ; :: thesis: H₅(p '&' q) = H₃(H₅(p),H₅(q))
thus H₅(p '&' q) = H₃(H₅(p),H₅(q)) from CQC_LANG:sch 8(A1); :: thesis: verum

end;

let x be bound_QC-variable; :: thesis: Valid (All x,p),J = FOR_ALL x,(Valid p,J)
thus H₅( All x,p) = H₄(x,H₅(p)) from CQC_LANG:sch 9(A1); :: thesis: verum