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 )

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

proof

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

proof

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

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

x \ (y * y) = x \ y by A5;

hence (x \ y) \ y = x \ y by Th11; :: thesis: verum

end;x \ (y * y) = x \ y by A5;

hence (x \ y) \ y = x \ y by Th11; :: thesis: verum