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

( (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