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