let X be BCI-Algebra_with_Condition(S); :: thesis: for x being Element of X holds x |^ 2 = x * x
let x be Element of X; :: thesis: x |^ 2 = x * x
thus x |^ 2 = x |^ (1 + 1)
.= (x |^ 1) * x by Def6
.= x * x by Th21 ; :: thesis: verum