let X be BCI-algebra; :: thesis: for A being Ideal of X
for x being Element of X
for a being Element of A st x <= a holds
x in A
let A be Ideal of X; :: thesis: for x being Element of X
for a being Element of A st x <= a holds
x in A
let x be Element of X; :: thesis: for a being Element of A st x <= a holds
x in A
let a be Element of A; :: thesis: ( x <= a implies x in A )
assume x <= a ; :: thesis: x in A
then x \ a = 0. X ;
then x \ a in A by BCIALG_1:def 18;
hence x in A by BCIALG_1:def 18; :: thesis: verum