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