:: deftheorem defines satisfying_(N4) FUZIMPL3:def 10 :
for N being UnOp of [.0,1.] holds
( N is satisfying_(N4) iff N is continuous );