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

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