let X be set ; :: thesis: for a, b, c, d being Real st a <= b & c in ['a,b'] & d in ['a,b'] & ['a,b'] c= X holds
['(min (c,d)),(max (c,d))'] c= X
let a, b, c, d be Real; :: thesis: ( a <= b & c in ['a,b'] & d in ['a,b'] & ['a,b'] c= X implies ['(min (c,d)),(max (c,d))'] c= X )
assume ( a <= b & c in ['a,b'] & d in ['a,b'] ) ; :: thesis: ( not ['a,b'] c= X or ['(min (c,d)),(max (c,d))'] c= X )
then ['(min (c,d)),(max (c,d))'] c= ['a,b'] by Lm2;
hence ( not ['a,b'] c= X or ['(min (c,d)),(max (c,d))'] c= X ) ; :: thesis: verum