let X be BCK-algebra; :: thesis: ( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) )
thus ( X is BCK-positive-implicative BCK-algebra implies for x, y being Element of X holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) ) :: thesis: ( ( for x, y being Element of X holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) ) implies X is BCK-positive-implicative BCK-algebra )
proof
assume A1: X is BCK-positive-implicative BCK-algebra ; :: thesis: for x, y being Element of X holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x)))
for x, y being Element of X holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x)))
proof
let x, y be Element of X; :: thesis: (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x)))
(x \ (x \ y)) \ y = (x \ y) \ (x \ y) by BCIALG_1:7
.= 0. X by BCIALG_1:def 5 ;
then x \ (x \ y) <= y ;
then A2: (x \ (x \ y)) \ (y \ (y \ x)) <= y \ (y \ (y \ x)) by BCIALG_1:5;
(x \ (x \ y)) \ (x \ (x \ (y \ (y \ x)))) = (x \ (x \ (x \ (y \ (y \ x))))) \ (x \ y) by BCIALG_1:7
.= (x \ (y \ (y \ x))) \ (x \ y) by BCIALG_1:8
.= (x \ (x \ y)) \ (y \ (y \ x)) by BCIALG_1:7 ;
then (x \ (x \ y)) \ (x \ (x \ (y \ (y \ x)))) <= y \ x by A2, BCIALG_1:8;
then ((x \ (x \ y)) \ (x \ (x \ (y \ (y \ x))))) \ (y \ x) = 0. X ;
then A3: ((x \ (x \ y)) \ (y \ x)) \ (x \ (x \ (y \ (y \ x)))) = 0. X by BCIALG_1:7;
(y \ (y \ x)) \ x = (y \ x) \ (y \ x) by BCIALG_1:7
.= 0. X by BCIALG_1:def 5 ;
then y \ (y \ x) <= x ;
then (y \ (y \ x)) \ (y \ x) <= x \ (y \ x) by BCIALG_1:5;
then y \ (y \ x) <= x \ (y \ x) by A1, Th28;
then A4: (y \ (y \ x)) \ (x \ (y \ x)) = 0. X ;
(x \ (x \ (y \ (y \ x)))) \ (y \ (y \ x)) = (x \ (y \ (y \ x))) \ (x \ (y \ (y \ x))) by BCIALG_1:7
.= 0. X by BCIALG_1:def 5 ;
then (x \ (x \ (y \ (y \ x)))) \ (x \ (y \ x)) = 0. X by A4, BCIALG_1:3;
then x \ (x \ (y \ (y \ x))) <= x \ (y \ x) ;
then (x \ (x \ (y \ (y \ x)))) \ (x \ (y \ (y \ x))) <= (x \ (y \ x)) \ (x \ (y \ (y \ x))) by BCIALG_1:5;
then (x \ (x \ (y \ (y \ x)))) \ (x \ (y \ (y \ x))) <= (x \ (x \ (y \ (y \ x)))) \ (y \ x) by BCIALG_1:7;
then x \ (x \ (y \ (y \ x))) <= (x \ (x \ (y \ (y \ x)))) \ (y \ x) by A1, Th28;
then A5: (x \ (x \ (y \ (y \ x)))) \ ((x \ (x \ (y \ (y \ x)))) \ (y \ x)) = 0. X ;
(y \ (y \ x)) \ y = (y \ y) \ (y \ x) by BCIALG_1:7
.= (y \ x) ` by BCIALG_1:def 5
.= 0. X by BCIALG_1:def 8 ;
then y \ (y \ x) <= y ;
then x \ y <= x \ (y \ (y \ x)) by BCIALG_1:5;
then x \ (x \ (y \ (y \ x))) <= x \ (x \ y) by BCIALG_1:5;
then (x \ (x \ (y \ (y \ x)))) \ (y \ x) <= (x \ (x \ y)) \ (y \ x) by BCIALG_1:5;
then ((x \ (x \ (y \ (y \ x)))) \ (y \ x)) \ ((x \ (x \ y)) \ (y \ x)) = 0. X ;
then (x \ (x \ (y \ (y \ x)))) \ ((x \ (x \ y)) \ (y \ x)) = 0. X by A5, BCIALG_1:3;
hence (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) by A3, BCIALG_1:def 7; :: thesis: verum
end;
hence for x, y being Element of X holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) ; :: thesis: verum
end;
assume A6: for x, y being Element of X holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) ; :: thesis: X is BCK-positive-implicative BCK-algebra
for x, y being Element of X holds x \ y = (x \ y) \ y
proof
let x, y be Element of X; :: thesis: x \ y = (x \ y) \ y
A7: (x \ y) \ ((x \ y) \ (x \ (x \ (x \ y)))) = (x \ y) \ ((x \ y) \ (x \ y)) by BCIALG_1:8
.= (x \ y) \ (0. X) by BCIALG_1:def 5
.= x \ y by BCIALG_1:2 ;
((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y)) = ((x \ y) \ ((x \ x) \ y)) \ (x \ (x \ y)) by BCIALG_1:7
.= ((x \ y) \ (y `)) \ (x \ (x \ y)) by BCIALG_1:def 5
.= ((x \ y) \ (0. X)) \ (x \ (x \ y)) by BCIALG_1:def 8
.= (x \ y) \ (x \ (x \ y)) by BCIALG_1:2
.= (x \ (x \ (x \ y))) \ y by BCIALG_1:7
.= (x \ y) \ y by BCIALG_1:8 ;
hence x \ y = (x \ y) \ y by A6, A7; :: thesis: verum
end;
hence X is BCK-positive-implicative BCK-algebra by Th28; :: thesis: verum