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

hence X1 is Ideal of X by A2, BCIALG_1:def 18; :: thesis: verum

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

0. X in X1
by A1, Def5;
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;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

hence X1 is Ideal of X by A2, BCIALG_1:def 18; :: thesis: verum