let a, b, x, y be real number ; :: thesis: ( a <= 0 & x <= y implies (AffineMap a,b) . x >= (AffineMap a,b) . y )
assume that
A1: a <= 0 and
A2: x <= y ; :: thesis: (AffineMap a,b) . x >= (AffineMap a,b) . y
A3: (AffineMap a,b) . x = (a * x) + b by Def3;
A4: (AffineMap a,b) . y = (a * y) + b by Def3;
a * x >= a * y by A1, A2, XREAL_1:67;
hence (AffineMap a,b) . x >= (AffineMap a,b) . y by A3, A4, XREAL_1:9; :: thesis: verum