let a, b be real number ; :: 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
abs (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 abs (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 abs (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 5;
hence ( not ['a,b'] c= dom f or not f is_integrable_on ['a,b'] or not f | ['a,b'] is bounded or abs (integral f,a,b) <= integral (abs f),a,b ) by Th7; :: thesis: verum