let X be BCI-algebra; for I being Ideal of X holds
( I is p-ideal of X iff for x, y, z being Element of X st (x \ z) \ (y \ z) in I holds
x \ y in I )
let I be Ideal of X; ( I is p-ideal of X iff for x, y, z being Element of X st (x \ z) \ (y \ z) in I holds
x \ y in I )
thus
( I is p-ideal of X implies for x, y, z being Element of X st (x \ z) \ (y \ z) in I holds
x \ y in I )
( ( for x, y, z being Element of X st (x \ z) \ (y \ z) in I holds
x \ y in I ) implies I is p-ideal of X )
assume A3:
for x, y, z being Element of X st (x \ z) \ (y \ z) in I holds
x \ y in I
; I is p-ideal of X
A4:
for x, y, z being Element of X st (x \ z) \ (y \ z) in I & y in I holds
x in I
0. X in I
by BCIALG_1:def 18;
hence
I is p-ideal of X
by A4, Def5; verum