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