let X be BCI-algebra; :: thesis: for x being Element of X holds x \ ((x `) `) is positive Element of X
let x be Element of X; :: thesis: x \ ((x `) `) is positive Element of X
(x \ ((x `) `)) ` = (x `) \ (((x `) `) `) by BCIALG_1:9
.= (x `) \ (x `) by BCIALG_1:8
.= 0. X by BCIALG_1:def 5 ;
then 0. X <= x \ ((x `) `) ;
hence x \ ((x `) `) is positive Element of X by Def2; :: thesis: verum