:: deftheorem N1Def defines satisfying_(N1) FUZIMPL3:def 4 :
for N being UnOp of [.0,1.] holds
( N is satisfying_(N1) iff ( N . 0 = 1 & N . 1 = 0 ) );