let a, b, c, x be Real; :: thesis:
assume that
A1: ( a < b & b < c ) and
A2: not x in ].a,c.[ ; :: thesis:
A6s: ( b - a > a - a & c - b > b - b ) by A1, XREAL_1:9;
a < c by XXREAL_0:2, A1;
then A7s: a - a < c - a by XREAL_1:9;
set p = 1 / (b - a);
set q = - (a / (b - a));
set s = - (1 / (c - b));
set t = c / (c - b);
A3: ((c / (c - b)) - (- (a / (b - a)))) / ((1 / (b - a)) - (- (1 / (c - b)))) = ((c / (c - b)) - (- (a / (b - a)))) / ((1 / (b - a)) + (1 / (c - b)))
.= ((c / (c - b)) + (a / (b - a))) / (((1 * (c - b)) + (1 * (b - a))) / ((b - a) * (c - b))) by XCMPLX_1:116, A6s
.= (((c * (b - a)) + (a * (c - b))) / ((c - b) * (b - a))) / (((1 * (c - b)) + (1 * (b - a))) / ((b - a) * (c - b))) by XCMPLX_1:116, A6s
.= ((b * (c - a)) / ((c - b) * (b - a))) / ((c - a) / ((b - a) * (c - b)))
.= (b * ((c - a) / ((c - b) * (b - a)))) / ((c - a) / ((b - a) * (c - b))) by XCMPLX_1:74
.= b * (((c - a) / ((c - b) * (b - a))) / ((c - a) / ((b - a) * (c - b)))) by XCMPLX_1:74
.= b * 1 by XCMPLX_1:60, A7s, A6s
.= b ;
A4: - ((- (a / (b - a))) / (1 / (b - a))) = - (((- a) / (b - a)) / (1 / (b - a))) by XCMPLX_1:187
.= (- ((- a) / (b - a))) / (1 / (b - a)) by XCMPLX_1:187
.= (a / (b - a)) / (1 / (b - a)) by XCMPLX_1:190
.= (a / (b - a)) * (b - a) by XCMPLX_1:100
.= a by XCMPLX_1:87, A6s ;
- ((c / (c - b)) / (- (1 / (c - b)))) = (c / (c - b)) / (1 / (c - b)) by XCMPLX_1:189
.= (c / (c - b)) * (c - b) by XCMPLX_1:100
.= c by XCMPLX_1:87, A6s ;
then ( (1 / (b - a)) * (- (1 / (c - b))) < 0 & 1 / (b - a) > 0 & (((1 / (b - a)) * (c / (c - b))) - ((- (a / (b - a))) * (- (1 / (c - b))))) / ((1 / (b - a)) - (- (1 / (c - b)))) > 0 & not x in ].(- ((- (a / (b - a))) / (1 / (b - a)))),(- ((c / (c - b)) / (- (1 / (c - b))))).[ ) by Th17, A1, A4, A2;
hence (((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | ].-infty,b.]) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,+infty.[)) . x <= 0 by A3, Th15; :: thesis: