let a, b, c be Real; :: thesis: ( a < b & b < c implies TriangularFS (a,b,c) is Lipschitzian )
assume A1: ( a < b & b < c ) ; :: thesis: TriangularFS (a,b,c) is Lipschitzian
then B5: c - b > b - b by XREAL_1:9;
set a1 = 1 / (b - a);
set p1 = 1 / (c - b);
set b1 = - (a / (b - a));
set q1 = c / (c - b);
c > a by A1, XXREAL_0:2;
then B4: c - a > a - a by XREAL_1:9;
B7: b - a > a - a by XREAL_1:9, A1;
((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 * (b - a)) + (a * (c - b))) / ((b - a) * (c - b))) / ((1 / (b - a)) + (1 / (c - b))) by XCMPLX_1:116, B5, B7
.= (((((c * b) - (c * a)) + (a * c)) - (a * b)) / ((b - a) * (c - b))) / (((1 * (b - a)) + (1 * (c - b))) / ((b - a) * (c - b))) by XCMPLX_1:116, B5, B7
.= ((c - a) * b) / (c - a) by XCMPLX_1:55, B5, B7
.= b by XCMPLX_1:89, B4 ;
then for x being Real holds (TriangularFS (a,b,c)) . x = max (0,(min (1,((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | ].-infty,(((c / (c - b)) - (- (a / (b - a)))) / ((1 / (b - a)) + (1 / (c - b)))).[) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.(((c / (c - b)) - (- (a / (b - a)))) / ((1 / (b - a)) + (1 / (c - b)))),+infty.[)) . x)))) by asymTT9, A1;
hence TriangularFS (a,b,c) is Lipschitzian by asymTT5, B7, B5; :: thesis: verum