let X be BCK-algebra; :: thesis:
thus ( X is BCK-implicative BCK-algebra implies ( X is commutative BCK-algebra & X is BCK-positive-implicative BCK-algebra ) ) :: thesis:
proof
assume A1: X is BCK-implicative BCK-algebra ; :: thesis:
A2: for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x)
proof
let x, y be Element of X; :: thesis: x \ (x \ y) <= 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 (x \ (x \ y)) \ (y \ x) <= y \ (y \ x) by BCIALG_1:5;
then (x \ (y \ x)) \ (x \ y) <= y \ (y \ x) by BCIALG_1:7;
hence x \ (x \ y) <= y \ (y \ x) by ; :: thesis: verum
end;
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
(x \ y) \ (y \ (x \ y)) = x \ y by ;
hence x \ y = (x \ y) \ y by ; :: thesis: verum
end;
hence ( X is commutative BCK-algebra & X is BCK-positive-implicative BCK-algebra ) by ; :: thesis: verum
end;
assume that
A3: X is commutative BCK-algebra and
A4: X is BCK-positive-implicative BCK-algebra ; :: thesis:
for x, y being Element of X holds x \ (y \ x) = x
proof
let x, y be Element of X; :: thesis: x \ (y \ x) = x
x \ (x \ (x \ (y \ x))) = x \ (y \ x) by BCIALG_1:8;
then A5: x \ (y \ x) = x \ ((y \ x) \ ((y \ x) \ x)) by ;
(y \ x) \ ((y \ x) \ x) = (y \ x) \ (y \ x) by
.= 0. X by BCIALG_1:def 5 ;
hence x \ (y \ x) = x by ; :: thesis: verum
end;
hence X is BCK-implicative BCK-algebra by Def12; :: thesis: verum