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 IT holds { z where z is Element of X : z \ x <= y } c= IT

let IT be non empty Subset of X; :: thesis: ( IT is Ideal of X implies for x, y being Element of IT holds { z where z is Element of X : z \ x <= y } c= IT )

assume A1: IT is Ideal of X ; :: thesis: for x, y being Element of IT holds { z where z is Element of X : z \ x <= y } c= IT

let x, y be Element of IT; :: thesis: { z where z is Element of X : z \ x <= y } c= IT

A2: 0. X in IT by A1, Def18;

let ss be object ; :: according to TARSKI:def 3 :: thesis: ( not ss in { z where z is Element of X : z \ x <= y } or ss in IT )

assume ss in { z where z is Element of X : z \ x <= y } ; :: thesis: ss in IT

then A3: ex z being Element of X st

( ss = z & z \ x <= y ) ;

then reconsider ss = ss as Element of X ;

(ss \ x) \ y in IT by A2, A3;

then ss \ x in IT by A1, Def18;

hence ss in IT by A1, Def18; :: thesis: verum

for x, y being Element of IT holds { z where z is Element of X : z \ x <= y } c= IT

let IT be non empty Subset of X; :: thesis: ( IT is Ideal of X implies for x, y being Element of IT holds { z where z is Element of X : z \ x <= y } c= IT )

assume A1: IT is Ideal of X ; :: thesis: for x, y being Element of IT holds { z where z is Element of X : z \ x <= y } c= IT

let x, y be Element of IT; :: thesis: { z where z is Element of X : z \ x <= y } c= IT

A2: 0. X in IT by A1, Def18;

let ss be object ; :: according to TARSKI:def 3 :: thesis: ( not ss in { z where z is Element of X : z \ x <= y } or ss in IT )

assume ss in { z where z is Element of X : z \ x <= y } ; :: thesis: ss in IT

then A3: ex z being Element of X st

( ss = z & z \ x <= y ) ;

then reconsider ss = ss as Element of X ;

(ss \ x) \ y in IT by A2, A3;

then ss \ x in IT by A1, Def18;

hence ss in IT by A1, Def18; :: thesis: verum