theorem Th63: :: BCIALG_1:63

for X being BCI-algebra holds
( X is p-Semisimple iff for x, y being Element of X holds x \ (y `) = y \ (x `) )