theorem Th5: :: BCIIDEAL:5

for X being BCI-algebra
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