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