let a, b, c, d be Real; :: thesis: ( a <= b & c in ['a,b'] & d in ['a,b'] implies ['(min (c,d)),(max (c,d))'] c= ['a,b'] )
assume A1: ( a <= b & c in ['a,b'] & d in ['a,b'] ) ; :: thesis: ['(min (c,d)),(max (c,d))'] c= ['a,b']
then ['a,b'] = [.a,b.] by INTEGRA5:def 3;
then A2: ( a <= c & d <= b & a <= d & c <= b ) by A1, XXREAL_1:1;

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

suppose A3: c <= d ; :: thesis: ['(min (c,d)),(max (c,d))'] c= ['a,b']

then A4: ( c = min (c,d) & d = max (c,d) ) by XXREAL_0:def 9, XXREAL_0:def 10;
( ['c,b'] c= ['a,b'] & ['c,d'] c= ['c,b'] ) by A2, A3, INTEGR19:1;
hence ['(min (c,d)),(max (c,d))'] c= ['a,b'] by A4; :: thesis: verum

end;

suppose A6: not c <= d ; :: thesis: ['(min (c,d)),(max (c,d))'] c= ['a,b']

then A7: ( d = min (c,d) & c = max (c,d) ) by XXREAL_0:def 9, XXREAL_0:def 10;
( ['d,b'] c= ['a,b'] & ['d,c'] c= ['d,b'] ) by A2, A6, INTEGR19:1;
hence ['(min (c,d)),(max (c,d))'] c= ['a,b'] by A7; :: thesis: verum

end;

end;