let X be BCI-Algebra_with_Condition(S); :: thesis: for x, y, z being Element of X holds
( x \ y <= z iff x <= y * z )
A1: for x, y, z being Element of X st x <= y * z holds
x \ y <= z

proof

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

end;

for x, y, z being Element of X st x \ y <= z holds
x <= y * z

proof

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

end;

hence for x, y, z being Element of X holds
( x \ y <= z iff x <= y * z ) by A1; :: thesis: verum