for X being BCI-algebra
for X1 being non empty Subset of X st X1 is associative-ideal of X holds
X1 is Ideal of X