let X be non empty BCIStr_1 ; :: thesis: ( X is BCI-algebra & ( for x, y being Element of X holds
( (x * y) \ x <= y & ( for t being Element of X st t \ x <= y holds
t <= x * y ) ) ) implies X is BCI-Algebra_with_Condition(S) )

assume that
A1: X is BCI-algebra and
A2: for x, y being Element of X holds
( (x * y) \ x <= y & ( for t being Element of X st t \ x <= y holds
t <= x * y ) ) ; :: thesis:
for x, y, z being Element of X holds (x \ y) \ z = x \ (y * z)
proof
let x, y, z be Element of X; :: thesis: (x \ y) \ z = x \ (y * z)
(y * z) \ y <= z by A2;
then A3: ((y * z) \ y) \ z = 0. X ;
(x \ ((x \ y) \ z)) \ y = (x \ y) \ ((x \ y) \ z) by
.= ((x \ y) \ (0. X)) \ ((x \ y) \ z) by ;
then ((x \ ((x \ y) \ z)) \ y) \ (z \ (0. X)) = 0. X by ;
then (x \ ((x \ y) \ z)) \ y <= z \ (0. X) ;
then (x \ ((x \ y) \ z)) \ y <= z by ;
then x \ ((x \ y) \ z) <= y * z by A2;
then (x \ ((x \ y) \ z)) \ (y * z) = 0. X ;
then A4: (x \ (y * z)) \ ((x \ y) \ z) = 0. X by ;
((x \ y) \ (x \ (y * z))) \ ((y * z) \ y) = 0. X by ;
then ((x \ y) \ (x \ (y * z))) \ z = 0. X by ;
then ((x \ y) \ z) \ (x \ (y * z)) = 0. X by ;
hence (x \ y) \ z = x \ (y * z) by ; :: thesis: verum
end;
hence X is BCI-Algebra_with_Condition(S) by ; :: thesis: verum