let X be BCK-Algebra_with_Condition(S); :: thesis: for x, y being Element of X holds (x \ y) * (y \ x) <= x * y
for x, y being Element of X holds (x \ y) * (y \ x) <= x * y

proof

let x, y be Element of X; :: thesis: (x \ y) * (y \ x) <= x * y
((x \ y) * (y \ x)) \ (x \ y) <= y \ x by Lm2;
then A1: (((x \ y) * (y \ x)) \ (x \ y)) \ y <= (y \ x) \ y by BCIALG_1:5;
(y \ x) \ y = (y \ y) \ x by BCIALG_1:7
.= x ` by BCIALG_1:def 5
.= 0. X by BCIALG_1:def 8 ;
then ((x \ y) * (y \ x)) \ ((x \ y) * y) <= 0. X by A1, Th11;
then (((x \ y) * (y \ x)) \ ((x \ y) * y)) \ (0. X) = 0. X ;
then A2: ((x \ y) * (y \ x)) \ ((x \ y) * y) = 0. X by BCIALG_1:2;
(y * (x \ y)) \ y <= x \ y by Lm2;
then A3: ((y * (x \ y)) \ y) \ x <= (x \ y) \ x by BCIALG_1:5;
(x \ y) \ x = (x \ x) \ y by BCIALG_1:7
.= y ` by BCIALG_1:def 5
.= 0. X by BCIALG_1:def 8 ;
then (y * (x \ y)) \ (y * x) <= 0. X by A3, Th11;
then ((y * (x \ y)) \ (y * x)) \ (0. X) = 0. X ;
then A4: (y * (x \ y)) \ (y * x) = 0. X by BCIALG_1:2;
(x \ y) * y = y * (x \ y) by Th6;
then ((x \ y) * (y \ x)) \ (y * x) = 0. X by A2, A4, BCIALG_1:3;
then (x \ y) * (y \ x) <= y * x ;
hence (x \ y) * (y \ x) <= x * y by Th6; :: thesis: verum

end;

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