:: deftheorem defines involutive PARTIT_2:def 3 :
for X being non empty set
for f being UnOp of X holds
( f is involutive iff for x being Element of X holds f . (f . x) = x );