theorem :: FCONT_1:54

for a, b, x, y being Real st a <= 0 & x <= y holds
(AffineMap (a,b)) . x >= (AffineMap (a,b)) . y