:: deftheorem defines 'not' MARGREL1:def 13 :
for v being boolean object holds
( ( v = FALSE implies 'not' v = TRUE ) & ( not v = FALSE implies 'not' v = FALSE ) );