:: deftheorem Def6 defines involutive ROBBINS3:def 6 :
for L being non empty ComplStr holds
( L is involutive iff for x being Element of L holds (x `) ` = x );