theorem Th3: :: BCIALG_6:3

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