let X be BCI-algebra; :: thesis: ( ( for x being Element of X holds x ` <= x ) iff for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) )
thus ( ( for x being Element of X holds x ` <= x ) implies for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) ) :: thesis: ( ( for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) ) 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, z being Element of X holds (x \ y) \ z <= x \ (y \ z)
let x, y, z be Element of X; :: thesis: (x \ y) \ z <= x \ (y \ z)
(x \ (x \ (y \ z))) \ (y \ z) = 0. X by Th1;
then A2: ((x \ (x \ (y \ z))) \ y) \ ((y \ z) \ y) = 0. X by Th4;
((x \ y) \ z) \ (x \ (y \ z)) = ((x \ y) \ (x \ (y \ z))) \ z by Th7
.= ((x \ (x \ (y \ z))) \ y) \ z by Th7 ;
then (((x \ y) \ z) \ (x \ (y \ z))) \ (((y \ z) \ y) \ z) = 0. X by A2, Th4;
then A3: (((x \ y) \ z) \ (x \ (y \ z))) \ (((y \ y) \ z) \ z) = 0. X by Th7;
z ` <= z by A1;
then (z `) \ z = 0. X ;
then (((x \ y) \ z) \ (x \ (y \ z))) \ (0. X) = 0. X by A3, Def5;
then ((x \ y) \ z) \ (x \ (y \ z)) = 0. X by Th2;
hence (x \ y) \ z <= x \ (y \ z) ; :: thesis: verum

end;

assume A4: for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) ; :: thesis: for x being Element of X holds x ` <= x
let x be Element of X; :: thesis: x ` <= x
((0. X) `) \ x <= (x `) ` by A4;
then x ` <= (x `) ` by Def5;
then (x `) \ ((x `) `) = 0. X ;
then (((x `) `) `) \ x = 0. X by Th7;
then (x `) \ x = 0. X by Th8;
hence x ` <= x ; :: thesis: verum