:: deftheorem Def44 defines Not_0 MODELC_2:def 44 :
for S being non empty set
for f being object
for b₃ being Element of ModelSP (Inf_seq S) holds
( b₃ = Not_0 (f,S) iff for t being set st t in Inf_seq S holds
( 'not' (Castboolean ((Fid (f,(Inf_seq S))) . t)) = TRUE iff (Fid (b₃,(Inf_seq S))) . t = TRUE ) );