theorem :: BCIALG_6:36

for X, X9 being BCI-algebra
for x, y being Element of X
for f being BCI-homomorphism of X,X9 st x <= y holds
f . x <= f . y