let a, b be Real; :: thesis: for f being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded holds
|.(integral (f,a,b)).| <= integral ((abs f),a,b)
let f be PartFunc of REAL,REAL; :: thesis: ( a <= b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded implies |.(integral (f,a,b)).| <= integral ((abs f),a,b) )
assume a <= b ; :: thesis: ( not ['a,b'] c= dom f or not f is_integrable_on ['a,b'] or not f | ['a,b'] is bounded or |.(integral (f,a,b)).| <= integral ((abs f),a,b) )
then ( integral (f,a,b) = integral (f,['a,b']) & integral ((abs f),a,b) = integral ((abs f),['a,b']) ) by INTEGRA5:def 4;
hence ( not ['a,b'] c= dom f or not f is_integrable_on ['a,b'] or not f | ['a,b'] is bounded or |.(integral (f,a,b)).| <= integral ((abs f),a,b) ) by Th7; :: thesis: verum