:: deftheorem Def43 defines Not_ MODELC_1:def 43 :
for S being non empty set
for b₂ being UnOp of (ModelSP S) holds
( b₂ = Not_ S iff for f being object st f in ModelSP S holds
b₂ . f = Not_0 (f,S) );