theorem :: BCIALG_4:20

for X being BCI-Algebra_with_Condition(S)
for x being Element of X holds x |^ 0 = 0. X by Def6;