theorem :: BCIALG_1:55

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