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:64;
( (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; :: thesis: verum