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

proof

assume A1: for x, y being Element of X holds y \ (y \ x) = x ; :: thesis: for x, y, z being Element of X holds (z \ y) \ (z \ x) = x \ y
let x, y, z be Element of X; :: thesis: (z \ y) \ (z \ x) = x \ y
(z \ y) \ (z \ x) = (z \ (z \ x)) \ y by Th7;
hence (z \ y) \ (z \ x) = x \ y by A1; :: thesis: verum

end;

assume A2: for x, y, z being Element of X holds (z \ y) \ (z \ x) = x \ y ; :: 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
(y \ (0. X)) \ (y \ x) = x \ (0. X) by A2;
then y \ (y \ x) = x \ (0. X) by Th2;
hence y \ (y \ x) = x by Th2; :: thesis: verum