let a, b, c, x be Real; :: thesis: ( a < b & b < c & x in [.a,c.] implies (TriangularFS (a,b,c)) . x >= 0 )
assume A1: ( a < b & b < c & x in [.a,c.] ) ; :: thesis: (TriangularFS (a,b,c)) . x >= 0
then A2s: ( b - a > a - a & c - b > b - b ) by XREAL_1:9;
D11: ( a <= x & x <= c ) by XXREAL_1:1, A1;
then CXs: ( a - a <= x - a & x - x <= c - x ) by XREAL_1:9;

per cases ( b < x or x <= b ) ;

suppose b < x ; :: thesis: (TriangularFS (a,b,c)) . x >= 0

then x in [.b,c.] by D11;
then (TriangularFS (a,b,c)) . x = (AffineMap ((- (1 / (c - b))),(c / (c - b)))) . x by A1, FUZZY_8:47
.= ((- (1 / (c - b))) * x) + (c / (c - b)) by FCONT_1:def 4
.= (- (x * (1 / (c - b)))) + (c / (c - b))
.= (- ((x * 1) / (c - b))) + (c / (c - b)) by XCMPLX_1:74
.= ((- x) / (c - b)) + (c / (c - b)) by XCMPLX_1:187
.= ((- x) + c) / (c - b) by XCMPLX_1:62
.= (c - x) / (c - b) ;
hence (TriangularFS (a,b,c)) . x >= 0 by A2s, CXs; :: thesis: verum

end;

suppose x <= b ; :: thesis: (TriangularFS (a,b,c)) . x >= 0

then x in [.a,b.] by D11;
then (TriangularFS (a,b,c)) . x = (AffineMap ((1 / (b - a)),(- (a / (b - a))))) . x by A1, FUZZY_8:46
.= ((1 / (b - a)) * x) + (- (a / (b - a))) by FCONT_1:def 4
.= (x * (1 / (b - a))) - (a / (b - a))
.= ((x * 1) / (b - a)) - (a / (b - a)) by XCMPLX_1:74
.= (x / (b - a)) + (- (a / (b - a)))
.= (x / (b - a)) + ((- a) / (b - a)) by XCMPLX_1:187
.= (x + (- a)) / (b - a) by XCMPLX_1:62
.= (x - a) / (b - a) ;
hence (TriangularFS (a,b,c)) . x >= 0 by A2s, CXs; :: thesis: verum

end;

end;