:: deftheorem defines isotonic BCIALG_6:def 7 :
for X, X9 being BCI-algebra
for f being BCI-homomorphism of X,X9 holds
( f is isotonic iff for x, y being Element of X st x <= y holds
f . x <= f . y );