:: deftheorem Def5 defines p-ideal BCIIDEAL:def 5 :
for X being BCI-algebra
for b₂ being non empty Subset of X holds
( b₂ is p-ideal of X iff ( 0. X in b₂ & ( for x, y, z being Element of X st (x \ z) \ (y \ z) in b₂ & y in b₂ holds
x in b₂ ) ) );