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 )

x * y = y ) implies X is positive-implicative )

x * y = y ) by A1; :: thesis: verum

x * y = y )

A1: ( X is positive-implicative implies for x, y being Element of X st x <= y holds

x * y = y )

proof

( ( for x, y being Element of X st x <= y holds
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;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

x * y = y ) implies X is positive-implicative )

proof

hence
( X is positive-implicative iff for x, y being Element of X st x <= y holds
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

end;x * y = y ; :: thesis: X is positive-implicative

for x being Element of X holds x * x = x

proof

hence
X is positive-implicative
by Th44; :: thesis: verum
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;x \ x = 0. X by BCIALG_1:def 5;

then x <= x ;

hence x * x = x by A6; :: thesis: verum

x * y = y ) by A1; :: thesis: verum