let a, b, x, y be Real; ( a <= 0 & x <= y implies (AffineMap (a,b)) . x >= (AffineMap (a,b)) . y )
assume
( a <= 0 & x <= y )
; (AffineMap (a,b)) . x >= (AffineMap (a,b)) . y
then A1:
a * x >= a * y
by XREAL_1:65;
( (AffineMap (a,b)) . x = (a * x) + b & (AffineMap (a,b)) . y = (a * y) + b )
by Def4;
hence
(AffineMap (a,b)) . x >= (AffineMap (a,b)) . y
by A1, XREAL_1:7; verum