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

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

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

proof

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

let x, y, z be Element of X; :: thesis: (x * y) \ z = (x \ z) * (y \ z)

(((x * y) \ z) \ (x \ z)) \ ((x * y) \ x) = 0. X by BCIALG_1:def 3;

then ((x * y) \ z) \ (x \ z) <= (x * y) \ x ;

then (((x * y) \ z) \ (x \ z)) \ z <= ((x * y) \ x) \ z by BCIALG_1:5;

then A3: ((((x * y) \ z) \ (x \ z)) \ z) \ (((x * y) \ x) \ z) = 0. X ;

(x * y) \ x <= y by Lm2;

then ((x * y) \ x) \ z <= y \ z by BCIALG_1:5;

then A4: (((x * y) \ x) \ z) \ (y \ z) = 0. X ;

(x * y) \ z = (x * y) \ (z * z) by A2, Th44

.= ((x * y) \ z) \ z by Th11 ;

then ((x * y) \ z) \ (x \ z) = (((x * y) \ z) \ (x \ z)) \ z by BCIALG_1:7;

then (((x * y) \ z) \ (x \ z)) \ (y \ z) = 0. X by A3, A4, BCIALG_1:3;

then A5: ((x * y) \ z) \ ((x \ z) * (y \ z)) = 0. X by Th11;

y <= x * y by Th37;

then y \ z <= (x * y) \ z by BCIALG_1:5;

then ((x * y) \ z) * (y \ z) <= ((x * y) \ z) * ((x * y) \ z) by Th7;

then A6: (((x * y) \ z) * (y \ z)) \ (((x * y) \ z) * ((x * y) \ z)) = 0. X ;

x <= x * y by Th37;

then x \ z <= (x * y) \ z by BCIALG_1:5;

then (x \ z) * (y \ z) <= ((x * y) \ z) * (y \ z) by Th7;

then ((x \ z) * (y \ z)) \ (((x * y) \ z) * (y \ z)) = 0. X ;

then ((x \ z) * (y \ z)) \ (((x * y) \ z) * ((x * y) \ z)) = 0. X by A6, BCIALG_1:3;

then ((x \ z) * (y \ z)) \ ((x * y) \ z) = 0. X by A2, Th44;

hence (x * y) \ z = (x \ z) * (y \ z) by A5, BCIALG_1:def 7; :: thesis: verum

end;let x, y, z be Element of X; :: thesis: (x * y) \ z = (x \ z) * (y \ z)

(((x * y) \ z) \ (x \ z)) \ ((x * y) \ x) = 0. X by BCIALG_1:def 3;

then ((x * y) \ z) \ (x \ z) <= (x * y) \ x ;

then (((x * y) \ z) \ (x \ z)) \ z <= ((x * y) \ x) \ z by BCIALG_1:5;

then A3: ((((x * y) \ z) \ (x \ z)) \ z) \ (((x * y) \ x) \ z) = 0. X ;

(x * y) \ x <= y by Lm2;

then ((x * y) \ x) \ z <= y \ z by BCIALG_1:5;

then A4: (((x * y) \ x) \ z) \ (y \ z) = 0. X ;

(x * y) \ z = (x * y) \ (z * z) by A2, Th44

.= ((x * y) \ z) \ z by Th11 ;

then ((x * y) \ z) \ (x \ z) = (((x * y) \ z) \ (x \ z)) \ z by BCIALG_1:7;

then (((x * y) \ z) \ (x \ z)) \ (y \ z) = 0. X by A3, A4, BCIALG_1:3;

then A5: ((x * y) \ z) \ ((x \ z) * (y \ z)) = 0. X by Th11;

y <= x * y by Th37;

then y \ z <= (x * y) \ z by BCIALG_1:5;

then ((x * y) \ z) * (y \ z) <= ((x * y) \ z) * ((x * y) \ z) by Th7;

then A6: (((x * y) \ z) * (y \ z)) \ (((x * y) \ z) * ((x * y) \ z)) = 0. X ;

x <= x * y by Th37;

then x \ z <= (x * y) \ z by BCIALG_1:5;

then (x \ z) * (y \ z) <= ((x * y) \ z) * (y \ z) by Th7;

then ((x \ z) * (y \ z)) \ (((x * y) \ z) * (y \ z)) = 0. X ;

then ((x \ z) * (y \ z)) \ (((x * y) \ z) * ((x * y) \ z)) = 0. X by A6, BCIALG_1:3;

then ((x \ z) * (y \ z)) \ ((x * y) \ z) = 0. X by A2, Th44;

hence (x * y) \ z = (x \ z) * (y \ z) by A5, BCIALG_1:def 7; :: thesis: verum

proof

hence
( X is positive-implicative iff for x, y, z being Element of X holds (x * y) \ z = (x \ z) * (y \ z) )
by A1; :: thesis: verum
assume A7:
for x, y, z being Element of X holds (x * y) \ z = (x \ z) * (y \ z)
; :: thesis: X is positive-implicative

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

end;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) \ x = (x \ x) * (x \ x) by A7;

then (x * x) \ x = (0. X) * (x \ x) by BCIALG_1:def 5;

then (x * x) \ x = (0. X) * (0. X) by BCIALG_1:def 5;

then A8: (x * x) \ x = 0. X by Th8;

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 A8, BCIALG_1:def 7; :: thesis: verum

end;(x * x) \ x = (x \ x) * (x \ x) by A7;

then (x * x) \ x = (0. X) * (x \ x) by BCIALG_1:def 5;

then (x * x) \ x = (0. X) * (0. X) by BCIALG_1:def 5;

then A8: (x * x) \ x = 0. X by Th8;

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 A8, BCIALG_1:def 7; :: thesis: verum