let X be BCI-algebra; :: thesis: for I being Ideal of X st I is p-ideal of X holds

BCK-part X c= I

let I be Ideal of X; :: thesis: ( I is p-ideal of X implies BCK-part X c= I )

assume A1: I is p-ideal of X ; :: thesis: BCK-part X c= I

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in BCK-part X or x in I )

assume A2: x in BCK-part X ; :: thesis: x in I

then A3: ex x1 being Element of X st

( x = x1 & 0. X <= x1 ) ;

reconsider x = x as Element of X by A2;

(0. X) \ x = 0. X by A3;

then (0. X) \ ((0. X) \ x) = 0. X by BCIALG_1:2;

then A4: (x \ x) \ ((0. X) \ x) = 0. X by BCIALG_1:def 5;

0. X in I by A1, Def5;

hence x in I by A1, A4, Def5; :: thesis: verum

BCK-part X c= I

let I be Ideal of X; :: thesis: ( I is p-ideal of X implies BCK-part X c= I )

assume A1: I is p-ideal of X ; :: thesis: BCK-part X c= I

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in BCK-part X or x in I )

assume A2: x in BCK-part X ; :: thesis: x in I

then A3: ex x1 being Element of X st

( x = x1 & 0. X <= x1 ) ;

reconsider x = x as Element of X by A2;

(0. X) \ x = 0. X by A3;

then (0. X) \ ((0. X) \ x) = 0. X by BCIALG_1:2;

then A4: (x \ x) \ ((0. X) \ x) = 0. X by BCIALG_1:def 5;

0. X in I by A1, Def5;

hence x in I by A1, A4, Def5; :: thesis: verum