let X, X' be BCI-algebra; :: thesis: for x, y being Element of
for f being BCI-homomorphism of X,X' st x <= y holds
f . x <= f . y
let x, y be Element of ; :: thesis: for f being BCI-homomorphism of X,X' st x <= y holds
f . x <= f . y
let f be BCI-homomorphism of X,X'; :: 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, BCIALG_1:def 11
.= 0. X' by Th35 ;
hence f . x <= f . y by BCIALG_1:def 11; :: thesis: verum