:: deftheorem Def18 defines '&' MARGREL1:def 18 :
for p, q, b₃ being boolean-valued Function holds
( b₃ = p '&' q iff ( dom b₃ = (dom p) /\ (dom q) & ( for x being object st x in dom b₃ holds
b₃ . x = (p . x) '&' (q . x) ) ) );