let X be BCI-algebra; :: thesis: ( ( for x being Element of X holds (x `) ` = x ) iff for x, y being Element of X holds y \ (y \ x) = x )
thus ( ( for x being Element of X holds (x `) ` = x ) implies for x, y being Element of X holds y \ (y \ x) = x ) :: thesis: ( ( for x, y being Element of X holds y \ (y \ x) = x ) implies for x being Element of X holds (x `) ` = x )

proof

assume A1: for x being Element of X holds (x `) ` = x ; :: thesis: for x, y being Element of X holds y \ (y \ x) = x
let x, y be Element of X; :: thesis: y \ (y \ x) = x
A2: (y \ (y \ x)) \ x = 0. X by Th1;
x \ (y \ (y \ x)) = ((x \ (y \ (y \ x))) `) ` by A1
.= ((x `) \ ((y \ (y \ x)) `)) ` by Th9
.= (0. X) \ (((x `) \ ((y \ (y \ x)) `)) \ (0. X)) by Th2
.= (0. X) \ ((((0. X) \ x) \ ((y \ (y \ x)) `)) \ ((y \ (y \ x)) \ x)) by Th1
.= (0. X) \ (0. X) by Th1
.= 0. X by Def5 ;
hence y \ (y \ x) = x by A2, Def7; :: thesis: verum

end;

thus ( ( for x, y being Element of X holds y \ (y \ x) = x ) implies for x being Element of X holds (x `) ` = x ) ; :: thesis: verum