let X be BCI-algebra; :: thesis: for IT being non empty Subset of X st IT is Ideal of X holds

for x, y being Element of X st x in IT & y <= x holds

y in IT

let IT be non empty Subset of X; :: thesis: ( IT is Ideal of X implies for x, y being Element of X st x in IT & y <= x holds

y in IT )

assume A1: IT is Ideal of X ; :: thesis: for x, y being Element of X st x in IT & y <= x holds

y in IT

let x, y be Element of X; :: thesis: ( x in IT & y <= x implies y in IT )

assume that

A2: x in IT and

A3: y <= x ; :: thesis: y in IT

y \ (0. X) <= x by A3, Th2;

then A4: y in { z where z is Element of X : z \ (0. X) <= x } ;

0. X is Element of IT by A1, Def18;

then { z where z is Element of X : z \ (0. X) <= x } c= IT by A1, A2, Lm5;

hence y in IT by A4; :: thesis: verum

for x, y being Element of X st x in IT & y <= x holds

y in IT

let IT be non empty Subset of X; :: thesis: ( IT is Ideal of X implies for x, y being Element of X st x in IT & y <= x holds

y in IT )

assume A1: IT is Ideal of X ; :: thesis: for x, y being Element of X st x in IT & y <= x holds

y in IT

let x, y be Element of X; :: thesis: ( x in IT & y <= x implies y in IT )

assume that

A2: x in IT and

A3: y <= x ; :: thesis: y in IT

y \ (0. X) <= x by A3, Th2;

then A4: y in { z where z is Element of X : z \ (0. X) <= x } ;

0. X is Element of IT by A1, Def18;

then { z where z is Element of X : z \ (0. X) <= x } c= IT by A1, A2, Lm5;

hence y in IT by A4; :: thesis: verum