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) )

A1: ( X is positive-implicative implies for x, y being Element of X holds x * y = x * (y \ x) )

proof

( ( for x, y being Element of X holds x * y = x * (y \ x) ) implies X is positive-implicative )
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;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

proof

hence
( X is positive-implicative iff for x, y being Element of X holds x * y = x * (y \ x) )
by A1; :: thesis: verum
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

end;for x, y being Element of X holds (x \ y) \ y = x \ y

proof

hence
X is positive-implicative
; :: thesis: verum
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;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