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']
['a,b'] = [.a,b.] by A1, 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;
A5: ['c,b'] c= ['a,b'] by A2, Th1;
['c,d'] c= ['c,b'] by A2, A3, Th1;
hence ['(min (c,d)),(max (c,d))'] c= ['a,b'] by A4, A5; :: 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;
A8: ['d,b'] c= ['a,b'] by A2, Th1;
['d,c'] c= ['d,b'] by A2, A6, Th1;
hence ['(min (c,d)),(max (c,d))'] c= ['a,b'] by A7, A8; :: thesis: verum

end;

end;