let X be BCI-algebra; :: thesis: for x being Element of X holds x |^ 2 = x \ (x `)
let x be Element of X; :: thesis: x |^ 2 = x \ (x `)
x |^ 2 = x |^ (1 + 1)
.= x \ ((x |^ 1) `) by Def1 ;
hence x |^ 2 = x \ (x `) by Th4; :: thesis: verum