for X being BCI-algebra
for x being Element of X holds x |^ 0 = 0. X by Def1;