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

proof

let t be Element of X; :: thesis: ( t \ x <= y implies t <= x * y )
assume A2: t \ x <= y ; :: thesis: t <= x * y
t \ (x * y) = (t \ x) \ y by Def2
.= 0. X by A2, BCIALG_1:def 11 ;
hence t <= x * y by BCIALG_1:def 11; :: thesis: verum

end;

((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, BCIALG_1:def 11; :: thesis: verum