let X be BCI-algebra; :: thesis: ( X is p-Semisimple BCI-algebra implies X is weakly-positive-implicative BCI-algebra )

assume A1: X is p-Semisimple BCI-algebra ; :: thesis: X is weakly-positive-implicative BCI-algebra

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

assume A1: X is p-Semisimple BCI-algebra ; :: thesis: X is weakly-positive-implicative BCI-algebra

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

proof

hence
X is weakly-positive-implicative BCI-algebra
by Def23; :: thesis: verum
let x, y, z be Element of X; :: thesis: (x \ y) \ z = ((x \ z) \ z) \ (y \ z)

((x \ z) \ z) \ (y \ z) = (x \ z) \ y by A1, Lm11

.= (x \ z) \ (y \ (0. X)) by Th2

.= (x \ y) \ (z \ (0. X)) by A1, Lm9 ;

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

end;((x \ z) \ z) \ (y \ z) = (x \ z) \ y by A1, Lm11

.= (x \ z) \ (y \ (0. X)) by Th2

.= (x \ y) \ (z \ (0. X)) by A1, Lm9 ;

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