theorem :: HILBERT3:31

for p, q being Element of HP-WFF
for V being SetValuation holds SetVal (V,(p '&' q)) = [:(SetVal (V,p)),(SetVal (V,q)):] by Def2;