let X be BCI-Algebra_with_Condition(S); :: thesis: 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 ) )
let x, y be Element of X; :: thesis: ( (x * y) \ x <= y & ( for t being Element of X st t \ x <= y holds
t <= x * y ) )
A1: for t being Element of X st t \ x <= y holds
t <= x * y by Def2;
((x * y) \ x) \ y = (x * y) \ (x * y) by Def2
.= 0. X by BCIALG_1:def 5 ;
hence ( (x * y) \ x <= y & ( for t being Element of X st t \ x <= y holds
t <= x * y ) ) by A1; :: thesis: verum