let a, b, c be real number ; :: thesis: ( a <= c & c <= b implies ( c in ['a,b'] & ['a,c'] c= ['a,b'] & ['c,b'] c= ['a,b'] ) )
assume A1: ( a <= c & c <= b ) ; :: thesis: ( c in ['a,b'] & ['a,c'] c= ['a,b'] & ['c,b'] c= ['a,b'] )
then A2: a <= b by XXREAL_0:2;
A3: ( ['a,b'] = [.a,b.] & ['a,c'] = [.a,c.] & ['c,b'] = [.c,b.] ) by A1, INTEGRA5:def 4, XXREAL_0:2;
A4: c in [.a,b.] by A1, XXREAL_1:1;
hence c in ['a,b'] by A1, INTEGRA5:def 4, XXREAL_0:2; :: thesis: ( ['a,c'] c= ['a,b'] & ['c,b'] c= ['a,b'] )
( a in [.a,b.] & b in [.a,b.] ) by A2, XXREAL_1:1;
hence ( ['a,c'] c= ['a,b'] & ['c,b'] c= ['a,b'] ) by A3, A4, XXREAL_2:def 12; :: thesis: verum