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

proof

assume A2: X is positive-implicative ; :: thesis: for x being Element of X holds x * x = x
let x be Element of X; :: thesis: x * x = x
A3: (x * x) \ x <= x by Lm2;
(x * x) \ x = ((x * x) \ x) \ x by A2;
then (x * x) \ x <= x \ x by A3, BCIALG_1:5;
then ( x \ x = 0. X & ((x * x) \ x) \ (x \ x) = 0. X ) by BCIALG_1:def 5;
then A4: (x * x) \ x = 0. X by BCIALG_1:2;
x \ (x * x) = (x \ x) \ x by Th11
.= x ` by BCIALG_1:def 5
.= 0. X by BCIALG_1:def 8 ;
hence x * x = x by A4, BCIALG_1:def 7; :: thesis: verum

end;

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

proof

assume A5: for x being Element of X holds x * x = x ; :: thesis: X is positive-implicative
for x, y being Element of X holds (x \ y) \ y = x \ y

proof

let x, y be Element of X; :: thesis: (x \ y) \ y = x \ y
x \ (y * y) = x \ y by A5;
hence (x \ y) \ y = x \ y by Th11; :: thesis: verum

end;

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

end;

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