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 ` ) ` ) by BCIALG_1:def 11;
hence x \ ((x ` ) ` ) is positive Element of X by Def2; :: thesis: verum