:: deftheorem Def2 defines FOR_ALL VALUAT_1:def 2 :
for Al being QC-alphabet
for A being non empty set
for x being bound_QC-variable of Al
for p, b₅ being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds
( b₅ = FOR_ALL (x,p) iff for v being Element of Valuations_in (Al,A) holds b₅ . v = ALL { (p . v9) where v9 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds
v9 . y = v . y } );