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
then A2: 0. X in IT by Def18;
let x, y be Element of IT; :: thesis: { z where z is Element of X : z \ x <= y } c= IT
for ss being set st ss in { z where z is Element of X : z \ x <= y } holds
ss in IT

proof

let ss be set ; :: thesis: ( ss in { z where z is Element of X : z \ x <= y } implies ss in IT )
assume ss in { z where z is Element of X : z \ x <= y } ; :: thesis: ss in IT
then consider z being Element of X such that
A3: ( ss = z & z \ x <= y ) ;
reconsider ss = ss as Element of X by A3;
(ss \ x) \ y in IT by A2, A3, Def11;
then ss \ x in IT by A1, Def18;
hence ss in IT by A1, Def18; :: thesis: verum

end;

hence { z where z is Element of X : z \ x <= y } c= IT by TARSKI:def 3; :: thesis: verum