let X be set ; :: thesis: for a, b, c, d being Real st a <= c & c <= d & d <= b & ['a,b'] c= X holds

['c,d'] c= X

let a, b, c, d be Real; :: 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;

hence ['c,d'] c= X by A2; :: thesis: verum

['c,d'] c= X

let a, b, c, d be Real; :: 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;

hence ['c,d'] c= X by A2; :: thesis: verum