let p, q, s, t, x be Real; :: thesis: ( p * s < 0 & p > 0 & ((p * t) - (q * s)) / (p - s) > 0 & not x in ].(- (q / p)),(- (t / s)).[ implies (((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[)) . x <= 0 )
assume A1: ( p * s < 0 & p > 0 ) ; :: thesis: ( not ((p * t) - (q * s)) / (p - s) > 0 or x in ].(- (q / p)),(- (t / s)).[ or (((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[)) . x <= 0 )
assume A2: ((p * t) - (q * s)) / (p - s) > 0 ; :: thesis: ( x in ].(- (q / p)),(- (t / s)).[ or (((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[)) . x <= 0 )
assume not x in ].(- (q / p)),(- (t / s)).[ ; :: thesis: (((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[)) . x <= 0

per cases then ( x <= - (q / p) or - (t / s) <= x ) ;

suppose B1: x <= - (q / p) ; :: thesis: (((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[)) . x <= 0

then (- (q / p)) * p >= x * p by XREAL_1:64, A1;
then - ((q / p) * p) >= x * p ;
then - q >= x * p by XCMPLX_1:87, A1;
then B3s: (- q) + q >= (x * p) + q by XREAL_1:6;
B4s: - (q / p) < (t - q) / (p - s) by A1, A2, Th13;
then B4: x < (t - q) / (p - s) by B1, XXREAL_0:2;
B2: x in ].-infty,((t - q) / (p - s)).] by XXREAL_1:234, B1, XXREAL_0:2, B4s;
not x in dom ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[) by XXREAL_1:236, B4;
then (((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[)) . x = ((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) . x by FUNCT_4:11
.= (AffineMap (p,q)) . x by FUNCT_1:49, B2 ;
hence (((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[)) . x <= 0 by B3s, FCONT_1:def 4; :: thesis: verum

end;

suppose C1: - (t / s) <= x ; :: thesis: (((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[)) . x <= 0

C33: s < 0 by A1;
then x * s <= (- (t / s)) * s by C1, XREAL_1:65;
then x * s <= - ((t / s) * s) ;
then x * s <= - t by XCMPLX_1:87, C33;
then C3s: (x * s) + t <= (- t) + t by XREAL_1:6;
(t - q) / (p - s) < - (t / s) by A1, A2, Th13;
then C2: x in [.((t - q) / (p - s)),+infty.[ by XXREAL_1:236, C1, XXREAL_0:2;
then x in dom ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[) by FUNCT_2:def 1;
then (((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[)) . x = ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[) . x by FUNCT_4:13
.= (AffineMap (s,t)) . x by FUNCT_1:49, C2 ;
hence (((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[)) . x <= 0 by C3s, FCONT_1:def 4; :: thesis: verum

end;

end;