let X, X9 be BCI-algebra; :: thesis: for x, y being Element of X
for f being BCI-homomorphism of X,X9 st x <= y holds
f . x <= f . y
let x, y be Element of X; :: thesis: for f being BCI-homomorphism of X,X9 st x <= y holds
f . x <= f . y
let f be BCI-homomorphism of X,X9; :: thesis: ( x <= y implies f . x <= f . y )
assume A1: x <= y ; :: thesis: f . x <= f . y
(f . x) \ (f . y) = f . (x \ y) by Def6
.= f . (0. X) by A1
.= 0. X9 by Th35 ;
hence f . x <= f . y ; :: thesis: verum