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 )
A3: (y * x) \ y <= x by Lm2;
(x * y) \ y = (y * x) \ y by Th6
.= ((y * x) \ y) \ y by A2 ;
then (x * y) \ y <= x \ y by A3, BCIALG_1:5;
then A4: ((x * y) \ y) \ (x \ y) = 0. X ;
A5: y \ (x * y) = y \ (y * x) by Th6
.= (y \ y) \ x by Th11
.= x ` by BCIALG_1:def 5
.= 0. X by BCIALG_1:def 8 ;
assume x <= y ; :: thesis: x * y = y
then x \ y = 0. X ;
then (x * y) \ y = 0. X by A4, BCIALG_1:2;
hence x * y = y by A5, 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 A6: 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 ;
hence x * x = x by A6; :: thesis: verum

end;

hence X is positive-implicative by Th44; :: 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