let a, b, c be Real; :: thesis: ( a <= c & c <= b implies ( c in ['a,b'] & ['a,c'] c= ['a,b'] & ['c,b'] c= ['a,b'] ) )
assume that
A1: a <= c and
A2: c <= b ; :: thesis: ( c in ['a,b'] & ['a,c'] c= ['a,b'] & ['c,b'] c= ['a,b'] )
A3: c in [.a,b.] by A1, A2;
hence c in ['a,b'] by A1, A2, INTEGRA5:def 3, XXREAL_0:2; :: thesis: ( ['a,c'] c= ['a,b'] & ['c,b'] c= ['a,b'] )
A4: ['c,b'] = [.c,b.] by A2, INTEGRA5:def 3;
a <= b by A1, A2, XXREAL_0:2;
then A5: ( a in [.a,b.] & b in [.a,b.] ) ;
( ['a,b'] = [.a,b.] & ['a,c'] = [.a,c.] ) by A1, A2, INTEGRA5:def 3, XXREAL_0:2;
hence ( ['a,c'] c= ['a,b'] & ['c,b'] c= ['a,b'] ) by A4, A3, A5, XXREAL_2:def 12; :: thesis: verum