let X be BCK-Algebra_with_Condition(S); :: thesis: ( X is implicative iff ( X is commutative & X is positive-implicative ) )
thus ( X is implicative implies ( X is commutative & X is positive-implicative ) ) :: thesis: ( X is commutative & X is positive-implicative implies X is implicative )

proof

assume A1: X is implicative ; :: thesis: ( X is commutative & X is positive-implicative )
A2: X is commutative

proof

A3: 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 by BCIALG_1:def 11;
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 A1, Def15; :: thesis: verum

end;

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 \ (y \ x) & y \ (y \ x) <= x \ (x \ y) ) by A3;
then ( (x \ (x \ y)) \ (y \ (y \ x)) = 0. X & (y \ (y \ x)) \ (x \ (x \ y)) = 0. X ) by BCIALG_1:def 11;
hence x \ (x \ y) = y \ (y \ x) by BCIALG_1:def 7; :: thesis: verum

end;

hence X is commutative by Def9; :: thesis: verum

end;

X is positive-implicative

proof

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 A1, Def15;
hence x \ y = (x \ y) \ y by A1, Def15; :: thesis: verum

end;

hence X is positive-implicative by Def11; :: thesis: verum

end;

hence ( X is commutative & X is positive-implicative ) by A2; :: thesis: verum

end;

assume A4: ( X is commutative & X is positive-implicative ) ; :: thesis: X is implicative
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 A4, Def9;
(y \ x) \ ((y \ x) \ x) = (y \ x) \ (y \ x) by A4, Def11
.= 0. X by BCIALG_1:def 5 ;
hence x \ (y \ x) = x by A5, BCIALG_1:2; :: thesis: verum

end;

hence X is implicative by Def15; :: thesis: verum