:: deftheorem Def6 defines Valid VALUAT_1:def 6 :
for Al being QC-alphabet
for A being non empty set
for J being interpretation of Al,A
for p being Element of CQC-WFF Al
for b₅ being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds
( b₅ = Valid (p,J) iff ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st
( b₅ = F . p & F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE & ( for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = ll 'in' (J . P) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) ) ) );