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;

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 )
;

end;