let X be BCI-algebra; :: thesis: for X1 being non empty Subset of X st X1 is p-ideal of X holds
X1 is Ideal of X
let X1 be non empty Subset of X; :: thesis: ( X1 is p-ideal of X implies X1 is Ideal of X )
assume A1: X1 is p-ideal of X ; :: thesis: X1 is Ideal of X
A2: for x, y being Element of X st x \ y in X1 & y in X1 holds
x in X1

proof

let x, y be Element of X; :: thesis: ( x \ y in X1 & y in X1 implies x in X1 )
assume that
A3: x \ y in X1 and
A4: y in X1 ; :: thesis: x in X1
(x \ (0. X)) \ y in X1 by A3, BCIALG_1:2;
then (x \ (0. X)) \ (y \ (0. X)) in X1 by BCIALG_1:2;
hence x in X1 by A1, A4, Def5; :: thesis: verum

end;

0. X in X1 by A1, Def5;
hence X1 is Ideal of X by A2, BCIALG_1:def 18; :: thesis: verum