let a, b, c, d be Real; :: thesis: ( a < b & b < c & c < d implies TrapezoidalFS (a,b,c,d) is Lipschitzian )
assume A1: ( a < b & b < c & c < d ) ; :: thesis: TrapezoidalFS (a,b,c,d) is Lipschitzian
then A20: a - a < b - a by XREAL_1:9;
A30: c - c < d - c by XREAL_1:9, A1;
set a1 = 1 / (b - a);
set b1 = - (a / (b - a));
set p1 = 1 / (d - c);
set q1 = d / (d - c);
B5: ((d / (d - c)) - (- (a / (b - a)))) / ((1 / (b - a)) + (1 / (d - c))) = ((d / (d - c)) + (a / (b - a))) / ((1 / (b - a)) + (1 / (d - c)))
.= (((d * (b - a)) + (a * (d - c))) / ((d - c) * (b - a))) / ((1 / (b - a)) + (1 / (d - c))) by XCMPLX_1:116, A20, A30
.= (((((d * b) - (d * a)) + (a * d)) - (a * c)) / ((d - c) * (b - a))) / (((1 * (b - a)) + (1 * (d - c))) / ((d - c) * (b - a))) by XCMPLX_1:116, A20, A30
.= ((b * d) - (a * c)) / (((d - c) + b) - a) by XCMPLX_1:55, A20, A30 ;
for x being Real holds (TrapezoidalFS (a,b,c,d)) . x = max (0,(min (1,((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | ].-infty,(((b * d) - (a * c)) / (((d - c) + b) - a)).[) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.(((b * d) - (a * c)) / (((d - c) + b) - a)),+infty.[)) . x)))) by asymTT8, A1;
hence TrapezoidalFS (a,b,c,d) is Lipschitzian by asymTT5, A20, A30, B5; :: thesis: verum