:: deftheorem defines satisfying_(N5) FUZIMPL3:def 11 :
for N being UnOp of [.0,1.] holds
( N is satisfying_(N5) iff N is involutive );