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
then BB: 0. X in I by Def1;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in BCK-part X or x in I )
assume x in BCK-part X ; :: thesis: x in I
then consider x1 being Element of X such that
B1: ( x = x1 & 0. X <= x1 ) ;
reconsider x = x as Element of X by B1;
(0. X) \ x = 0. X by B1, BCIALG_1:def 11;
then (0. X) \ ((0. X) \ x) = 0. X by BCIALG_1:2;
then (x \ x) \ ((0. X) \ x) = 0. X by BCIALG_1:def 5;
hence x in I by Def1, A1, BB; :: thesis: verum