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

for x, y being Element of X holds (x \ y) * (y \ x) <= x * y

proof

hence
for x, y being Element of X holds (x \ y) * (y \ x) <= x * y
; :: thesis: verum
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;((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