let a, b, c, d be real number ; :: thesis: for n being non empty Element of NAT
for f being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
( |.f.| is_integrable_on ['(min (c,d)),(max (c,d))'] & |.f.| | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,(min (c,d)),(max (c,d))) )
let n be non empty Element of NAT ; :: thesis: for f being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
( |.f.| is_integrable_on ['(min (c,d)),(max (c,d))'] & |.f.| | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,(min (c,d)),(max (c,d))) )
let f be PartFunc of REAL,(REAL n); :: thesis: ( a <= b & f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies ( |.f.| is_integrable_on ['(min (c,d)),(max (c,d))'] & |.f.| | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,(min (c,d)),(max (c,d))) ) )
assume A1: ( a <= b & f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] ) ; :: thesis: ( |.f.| is_integrable_on ['(min (c,d)),(max (c,d))'] & |.f.| | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,(min (c,d)),(max (c,d))) )
A2: ( c is Real & d is Real ) by XREAL_0:def 1;

per cases ( not c <= d or c <= d ) ;

suppose A3: not c <= d ; :: thesis: ( |.f.| is_integrable_on ['(min (c,d)),(max (c,d))'] & |.f.| | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,(min (c,d)),(max (c,d))) )

then A4: ['d,c'] = [.d,c.] by INTEGRA5:def 3;
then integral (f,c,d) = - (integral (f,['d,c'])) by A2, INTEGR15:20;
then integral (f,c,d) = - (integral (f,d,c)) by A2, A4, INTEGR15:19;
then A5: |.(integral (f,c,d)).| = |.(integral (f,d,c)).| by EUCLID:10;
( d = min (c,d) & c = max (c,d) ) by A3, XXREAL_0:def 9, XXREAL_0:def 10;
hence ( |.f.| is_integrable_on ['(min (c,d)),(max (c,d))'] & |.f.| | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,(min (c,d)),(max (c,d))) ) by A1, A3, A5, Lm10; :: thesis: verum

end;

suppose A6: c <= d ; :: thesis: ( |.f.| is_integrable_on ['(min (c,d)),(max (c,d))'] & |.f.| | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,(min (c,d)),(max (c,d))) )

then ( c = min (c,d) & d = max (c,d) ) by XXREAL_0:def 9, XXREAL_0:def 10;
hence ( |.f.| is_integrable_on ['(min (c,d)),(max (c,d))'] & |.f.| | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,(min (c,d)),(max (c,d))) ) by A1, A6, Lm10; :: thesis: verum

end;

end;