:: deftheorem Def8 defines 'imp' BVFUNC_1:def 8 :
for A being non empty set
for p, q, b₄ being Function of A,BOOLEAN holds
( b₄ = p 'imp' q iff for x being Element of A holds b₄ . x = ('not' (p . x)) 'or' (q . x) );