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