:: deftheorem defines non-filling FUZIMPL3:def 15 :
for N being UnOp of [.0,1.] holds
( N is non-filling iff for x being Element of [.0,1.] holds
( N . x = 1 iff x = 0 ) );