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 ;
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 ;
hence x * y = y by ; :: 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:
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