:: deftheorem defines 'not' MARGREL1:def 19 :
for A being non empty set
for p, b₃ being Function of A,BOOLEAN holds
( b₃ = 'not' p iff for x being Element of A holds b₃ . x = 'not' (p . x) );