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

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