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