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