theorem Th5: :: BCIALG_6:5

for X being BCI-algebra
for x being Element of X holds x |^ (- 1) = x `