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 )

y in I ; :: thesis: I is p-ideal of X

A6: for x, y, z being Element of X st (x \ z) \ (y \ z) in I & y in I holds

x in I

hence I is p-ideal of X by A6, Def5; :: thesis: verum

( 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 A5:
for x, y being Element of X st x in I & x <= y holds
assume
I is p-ideal of X
; :: thesis: for x, y being Element of X st x in I & x <= y holds

y in I

then A1: BCK-part X c= I by Th19;

let x, y be Element of X; :: thesis: ( x in I & x <= y implies y in I )

assume that

A2: x in I and

A3: x <= y ; :: thesis: y in I

A4: x \ y = 0. X by A3;

then (y \ x) ` = x \ y by BCIALG_1:6;

then 0. X <= y \ x by A4;

then y \ x in BCK-part X ;

hence y in I by A2, A1, BCIALG_1:def 18; :: thesis: verum

end;y in I

then A1: BCK-part X c= I by Th19;

let x, y be Element of X; :: thesis: ( x in I & x <= y implies y in I )

assume that

A2: x in I and

A3: x <= y ; :: thesis: y in I

A4: x \ y = 0. X by A3;

then (y \ x) ` = x \ y by BCIALG_1:6;

then 0. X <= y \ x by A4;

then y \ x in BCK-part X ;

hence y in I by A2, A1, BCIALG_1:def 18; :: thesis: verum

y in I ; :: thesis: I is p-ideal of X

A6: for x, y, z being Element of X st (x \ z) \ (y \ z) in I & y in I holds

x in I

proof

0. X in I
by BCIALG_1:def 18;
let x, y, z be Element of X; :: thesis: ( (x \ z) \ (y \ z) in I & y in I implies x in I )

assume that

A7: (x \ z) \ (y \ z) in I and

A8: 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 ;

then x \ y in I by A5, A7;

hence x in I by A8, BCIALG_1:def 18; :: thesis: verum

end;assume that

A7: (x \ z) \ (y \ z) in I and

A8: 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 ;

then x \ y in I by A5, A7;

hence x in I by A8, BCIALG_1:def 18; :: thesis: verum

hence I is p-ideal of X by A6, Def5; :: thesis: verum