let a, b, c be Real; :: thesis: ( a < b implies ( ['a,b'] c= [#] REAL & lower_bound ['a,b'] = a & upper_bound ['a,b'] = b ) )
assume A1: a < b ; :: thesis: ( ['a,b'] c= [#] REAL & lower_bound ['a,b'] = a & upper_bound ['a,b'] = b )
R1: [#] REAL = REAL by SUBSET_1:def 3;
( ['a,b'] = [.(lower_bound ['a,b']),(upper_bound ['a,b']).] & ['a,b'] = [.a,b.] ) by A1, INTEGRA5:def 3, INTEGRA1:4;
hence ( ['a,b'] c= [#] REAL & lower_bound ['a,b'] = a & upper_bound ['a,b'] = b ) by INTEGRA1:5, R1; :: thesis: verum