let X be BCK-Algebra_with_Condition(S); :: thesis: ( X is positive-implicative iff for x, y being Element of X holds x * y = x * (y \ x) )
A1: ( X is positive-implicative implies for x, y being Element of X holds x * y = x * (y \ x) )
proof
assume A2: X is positive-implicative ; :: thesis: for x, y being Element of X holds x * y = x * (y \ x)
let x, y be Element of X; :: thesis: x * y = x * (y \ x)
(y \ x) \ y = (y \ y) \ x by BCIALG_1:7
.= x ` by BCIALG_1:def 5
.= 0. X by BCIALG_1:def 8 ;
then y \ x <= y ;
then x * (y \ x) <= x * y by Th7;
then A3: (x * (y \ x)) \ (x * y) = 0. X ;
(x * y) \ x = (x \ x) * (y \ x) by A2, Th46
.= (0. X) * (y \ x) by BCIALG_1:def 5
.= y \ x by Th8 ;
then ((x * y) \ x) \ (y \ x) = 0. X by BCIALG_1:def 5;
then (x * y) \ (x * (y \ x)) = 0. X by Th11;
hence x * y = x * (y \ x) by A3, BCIALG_1:def 7; :: thesis: verum
end;
( ( for x, y being Element of X holds x * y = x * (y \ x) ) implies X is positive-implicative )
proof
assume A4: for x, y being Element of X holds x * y = x * (y \ 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
y * y = y * (y \ y) by A4
.= y * (0. X) by BCIALG_1:def 5
.= y by Th8 ;
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, y being Element of X holds x * y = x * (y \ x) ) by A1; :: thesis: verum