let X be BCK-Algebra_with_Condition(S); :: thesis: ( X is positive-implicative iff for x, y being Element of X st x <= y holds
x * y = y )
A1: ( X is positive-implicative implies for x, y being Element of X st x <= y holds
x * y = y )

proof

assume A2: X is positive-implicative ; :: thesis: for x, y being Element of X st x <= y holds
x * y = y
let x, y be Element of X; :: thesis: ( x <= y implies x * y = y )
assume A3: x <= y ; :: thesis: x * y = y
A4: (x * y) \ y = (y * x) \ y by Th7
.= ((y * x) \ y) \ y by A2, Def11 ;
(y * x) \ y <= x by Lm2;
then (x * y) \ y <= x \ y by A4, BCIALG_1:5;
then A5: ((x * y) \ y) \ (x \ y) = 0. X by BCIALG_1:def 11;
x \ y = 0. X by A3, BCIALG_1:def 11;
then A6: (x * y) \ y = 0. X by A5, BCIALG_1:2;
y \ (x * y) = y \ (y * x) by Th7
.= (y \ y) \ x by Th12
.= x ` by BCIALG_1:def 5
.= 0. X by BCIALG_1:def 8 ;
hence x * y = y by A6, BCIALG_1:def 7; :: thesis: verum

end;

( ( for x, y being Element of X st x <= y holds
x * y = y ) implies X is positive-implicative )

proof

assume A7: for x, y being Element of X st x <= y holds
x * y = y ; :: thesis: X is positive-implicative
for x being Element of X holds x * x = x

proof

let x be Element of X; :: thesis: x * x = x
x \ x = 0. X by BCIALG_1:def 5;
then x <= x by BCIALG_1:def 11;
hence x * x = x by A7; :: thesis: verum

end;

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

end;

hence ( X is positive-implicative iff for x, y being Element of X st x <= y holds
x * y = y ) by A1; :: thesis: verum