:: deftheorem Def5 defines '&' ARMSTRNG:def 5 :
for n being Element of NAT
for p, q, b₄ being Tuple of n, BOOLEAN holds
( b₄ = p '&' q iff for i being set st i in Seg n holds
b₄ . i = (p /. i) '&' (q /. i) );