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