let X be BCI-algebra; :: thesis: ( X is p-Semisimple implies for x, y, z, u being Element of X holds
( (x \ u) \ (z \ y) = (y \ u) \ (z \ x) & (x \ u) \ (z \ y) = (x \ z) \ (u \ y) ) )
assume A1: X is p-Semisimple ; :: thesis: for x, y, z, u being Element of X holds
( (x \ u) \ (z \ y) = (y \ u) \ (z \ x) & (x \ u) \ (z \ y) = (x \ z) \ (u \ y) )
let x, y, z, u be Element of X; :: thesis: ( (x \ u) \ (z \ y) = (y \ u) \ (z \ x) & (x \ u) \ (z \ y) = (x \ z) \ (u \ y) )
A2: (x \ u) \ (z \ y) = (x \ (z \ y)) \ u by Th7
.= (y \ (z \ x)) \ u by A1, Th57 ;
(x \ u) \ (z \ y) = y \ (z \ (x \ u)) by A1, Th57
.= y \ (u \ (x \ z)) by A1, Th57
.= (x \ z) \ (u \ y) by A1, Th57 ;
hence ( (x \ u) \ (z \ y) = (y \ u) \ (z \ x) & (x \ u) \ (z \ y) = (x \ z) \ (u \ y) ) by A2, Th7; :: thesis: verum