:: deftheorem defines is_an_involution QMAX_1:def 6 :
for X1 being set
for Inv being Function of X1,X1 holds
( Inv is_an_involution iff for x1 being Element of X1 holds Inv . (Inv . x1) = x1 );