let A be non empty closed_interval Subset of REAL; :: thesis: for a, b, c being Real st a < b & b < c holds
( TriangularFS (a,b,c) is_integrable_on A & (TriangularFS (a,b,c)) | A is bounded )
let a, b, c be Real; :: thesis: ( a < b & b < c implies ( TriangularFS (a,b,c) is_integrable_on A & (TriangularFS (a,b,c)) | A is bounded ) )
assume A1: ( a < b & b < c ) ; :: thesis: ( TriangularFS (a,b,c) is_integrable_on A & (TriangularFS (a,b,c)) | A is bounded )
reconsider f = TriangularFS (a,b,c) as PartFunc of REAL,REAL ;
TriangularFS (a,b,c) is Lipschitzian by FUZZY_5:86, A1;
then A6: f | A is continuous ;
dom f = REAL by FUNCT_2:def 1;
hence ( TriangularFS (a,b,c) is_integrable_on A & (TriangularFS (a,b,c)) | A is bounded ) by INTEGRA5:11, INTEGRA5:10, A6; :: thesis: verum