let X be set ; :: thesis: for a, c, d, b being real number st a <= c & c <= d & d <= b & ['a,b'] c= X holds
['c,d'] c= X
let a, c, d, b be real number ; :: thesis: ( a <= c & c <= d & d <= b & ['a,b'] c= X implies ['c,d'] c= X )
assume that
A1: ( a <= c & c <= d & d <= b ) and
A2: ['a,b'] c= X ; :: thesis: ['c,d'] c= X
A3: ['c,d'] c= ['c,b'] by Th1, A1;
c <= b by A1, XXREAL_0:2;
then ['c,b'] c= ['a,b'] by Th1, A1;
then ['c,d'] c= ['a,b'] by A3, XBOOLE_1:1;
hence ['c,d'] c= X by A2, XBOOLE_1:1; :: thesis: verum