let X be BCI-algebra; :: thesis: for I being Ideal of X holds
( I is p-ideal of X iff for x, y being Element of X st x in I & x <= y holds
y in I )
let I be Ideal of X; :: thesis: ( I is p-ideal of X iff for x, y being Element of X st x in I & x <= y holds
y in I )
thus ( I is p-ideal of X implies for x, y being Element of X st x in I & x <= y holds
y in I ) :: thesis: ( ( for x, y being Element of X st x in I & x <= y holds
y in I ) implies I is p-ideal of X )

proof

assume A: I is p-ideal of X ; :: thesis: for x, y being Element of X st x in I & x <= y holds
y in I
let x, y be Element of X; :: thesis: ( x in I & x <= y implies y in I )
assume A2: ( x in I & x <= y ) ; :: thesis: y in I
AC: BCK-part X c= I by A, TL352;
A3: ( x \ y = 0. X & x in I ) by A2, BCIALG_1:def 11;
then (y \ x) ` = x \ y by BCIALG_1:6;
then 0. X <= y \ x by A3, BCIALG_1:def 11;
then y \ x in BCK-part X ;
hence y in I by A2, AC, BCIALG_1:def 18; :: thesis: verum

end;

assume B: for x, y being Element of X st x in I & x <= y holds
y in I ; :: thesis: I is p-ideal of X
B1: 0. X in I by BCIALG_1:def 18;
for x, y, z being Element of X st (x \ z) \ (y \ z) in I & y in I holds
x in I

proof

let x, y, z be Element of X; :: thesis: ( (x \ z) \ (y \ z) in I & y in I implies x in I )
assume C1: ( (x \ z) \ (y \ z) in I & y in I ) ; :: thesis: x in I
((x \ z) \ (y \ z)) \ (x \ y) = 0. X by BCIALG_1:def 3;
then (x \ z) \ (y \ z) <= x \ y by BCIALG_1:def 11;
then x \ y in I by C1, B;
hence x in I by C1, BCIALG_1:def 18; :: thesis: verum

end;

hence I is p-ideal of X by Def1, B1; :: thesis: verum