let X be BCI-algebra; :: thesis: ( X is p-Semisimple iff for x, z being Element of X holds ((x \ z) ` ) ` = x \ z )
thus ( X is p-Semisimple implies for x, z being Element of X holds ((x \ z) ` ) ` = x \ z ) :: thesis: ( ( for x, z being Element of X holds ((x \ z) ` ) ` = x \ z ) implies X is p-Semisimple )

proof

assume A1: X is p-Semisimple ; :: thesis: for x, z being Element of X holds ((x \ z) ` ) ` = x \ z
let x, z be Element of X; :: thesis: ((x \ z) ` ) ` = x \ z
((x \ z) ` ) ` = ((x ` ) \ (z ` )) ` by Th9
.= (z \ x) ` by A1, Th59
.= (z ` ) \ (x ` ) by Th9 ;
hence ((x \ z) ` ) ` = x \ z by A1, Th59; :: thesis: verum

end;

assume A2: for x, z being Element of X holds ((x \ z) ` ) ` = x \ z ; :: thesis: X is p-Semisimple

now

let x be Element of X; :: thesis: (x ` ) ` = x
((x \ (0. X)) ` ) ` = x \ (0. X) by A2;
then (x ` ) ` = x \ (0. X) by Th2;
hence (x ` ) ` = x by Th2; :: thesis: verum

end;

hence X is p-Semisimple by Th54; :: thesis: verum