let X be BCI-Algebra_with_Condition(S); :: thesis: for x, y, z being Element of X holds x \ y <= (x \ z) * (z \ y)
let x, y, z be Element of X; :: thesis: x \ y <= (x \ z) * (z \ y)
((x \ y) \ (x \ z)) \ (z \ y) = 0. X by BCIALG_1:11;
then (x \ y) \ ((x \ z) * (z \ y)) = 0. X by Th11;
hence x \ y <= (x \ z) * (z \ y) ; :: thesis: verum