theorem Th22: :: BCIALG_4:23

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