:: deftheorem Def42 defines Not_0 MODELC_1:def 42 :
for S being non empty set
for f being object
for b₃ being Element of ModelSP S holds
( b₃ = Not_0 (f,S) iff for s being set st s in S holds
( 'not' (Castboolean ((Fid (f,S)) . s)) = TRUE iff (Fid (b₃,S)) . s = TRUE ) );