:: deftheorem Def26 defines p-Semisimple BCIALG_1:def 26 :
for IT being BCI-algebra holds
( IT is p-Semisimple iff for x, y being Element of IT holds x \ (x \ y) = y );