let X be BCI-algebra; :: thesis: ( X is p-Semisimple implies ( X is BCI-commutative & X is BCI-weakly-commutative ) )
assume A1: X is p-Semisimple ; :: thesis: ( X is BCI-commutative & X is BCI-weakly-commutative )
A2: for x, y being Element of X holds (x \ (x \ y)) \ ((0. X) \ (x \ y)) = y \ (y \ x)

proof

let x, y be Element of X; :: thesis: (x \ (x \ y)) \ ((0. X) \ (x \ y)) = y \ (y \ x)
(0. X) \ (x \ y) = ((0. X) \ (0. X)) \ (x \ y) by BCIALG_1:def 5
.= ((0. X) \ x) \ ((0. X) \ y) by A1, BCIALG_1:64
.= (y \ x) \ ((0. X) \ (0. X)) by A1, BCIALG_1:58
.= (y \ x) \ (0. X) by BCIALG_1:def 5
.= y \ x by BCIALG_1:2 ;
hence (x \ (x \ y)) \ ((0. X) \ (x \ y)) = y \ (y \ x) by A1; :: thesis: verum

end;

for x, y being Element of X st x \ y = 0. X holds
x = y \ (y \ x) by A1;
hence ( X is BCI-commutative & X is BCI-weakly-commutative ) by A2; :: thesis: verum