let a, b, c be Real; :: thesis: ( a < b & b < c implies ( (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 ) )
assume A1: ( a < b & b < c ) ; :: thesis: ( (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 )
then a < c by XXREAL_0:2;
then A4s: a - a < c - a by XREAL_1:9;
A2s: ( b - a > a - a & c - b > b - b ) by A1, XREAL_1:9;
(((1 / (b - a)) * (c / (c - b))) - ((- (a / (b - a))) * (- (1 / (c - b))))) / ((1 / (b - a)) - (- (1 / (c - b)))) = (((1 * c) / ((b - a) * (c - b))) - ((a / (b - a)) * (1 / (c - b)))) / ((1 / (b - a)) + (1 / (c - b))) by XCMPLX_1:76
.= ((c / ((b - a) * (c - b))) - ((a * 1) / ((b - a) * (c - b)))) / ((1 / (b - a)) + (1 / (c - b))) by XCMPLX_1:76
.= ((c / ((b - a) * (c - b))) - ((a * 1) / ((b - a) * (c - b)))) / (((1 * (c - b)) + (1 * (b - a))) / ((b - a) * (c - b))) by XCMPLX_1:116, A2s
.= ((c - a) / ((b - a) * (c - b))) / ((c - a) / ((b - a) * (c - b))) by XCMPLX_1:120
.= 1 by XCMPLX_1:60, A2s, A4s ;
hence ( (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 ) by A2s; :: thesis: verum