:: deftheorem Def2 defines SetVal HILBERT3:def 2 :
for V being SetValuation
for b₂ being ManySortedSet of HP-WFF holds
( b₂ = SetVal V iff ( b₂ . VERUM = 1 & ( for n being Element of NAT holds b₂ . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds
( b₂ . (p '&' q) = [:(b₂ . p),(b₂ . q):] & b₂ . (p => q) = Funcs ((b₂ . p),(b₂ . q)) ) ) ) );