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 )

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

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 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
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;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

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