theorem Th9: :: HILBERT4:4

for A being set
for f being involutive Function of A,A holds f * f = id A