theorem Th21: :: BCIALG_4:22

for X being BCI-Algebra_with_Condition(S)
for x being Element of X holds x |^ 1 = x