let a, b, x, y be Real; :: thesis: ( a < 0 & x < y implies (AffineMap (a,b)) . x > (AffineMap (a,b)) . y )
assume ( a < 0 & x < y ) ; :: thesis: (AffineMap (a,b)) . x > (AffineMap (a,b)) . y
then A1: a * x > a * y by XREAL_1:69;
( (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:8; :: thesis: verum