:: deftheorem Def17 defines 'not' MARGREL1:def 17 :
for p, b₂ being boolean-valued Function holds
( b₂ = 'not' p iff ( dom b₂ = dom p & ( for x being object st x in dom p holds
b₂ . x = 'not' (p . x) ) ) );