let a, b, c, d be Real; :: thesis: ( b <= c implies [.a,b.] /\ [.c,d.] c= [.b,b.] )
assume A1: b <= c ; :: thesis: [.a,b.] /\ [.c,d.] c= [.b,b.]

per cases ( a <= b or b < a ) ;

suppose A2: a <= b ; :: thesis: [.a,b.] /\ [.c,d.] c= [.b,b.]

per cases ( c <= d or d < c ) ;

suppose c <= d ; :: thesis: [.a,b.] /\ [.c,d.] c= [.b,b.]

then b <= d by A1, XXREAL_0:2;
then [.a,b.] /\ [.b,d.] = [.b,b.] by A2, XXREAL_1:143;
hence [.a,b.] /\ [.c,d.] c= [.b,b.] by A1, XBOOLE_1:26, XXREAL_1:34; :: thesis: verum

end;

suppose d < c ; :: thesis: [.a,b.] /\ [.c,d.] c= [.b,b.]

then [.c,d.] = {} by XXREAL_1:29;
hence [.a,b.] /\ [.c,d.] c= [.b,b.] ; :: thesis: verum

end;

end;

end;

suppose b < a ; :: thesis: [.a,b.] /\ [.c,d.] c= [.b,b.]

then [.a,b.] = {} by XXREAL_1:29;
hence [.a,b.] /\ [.c,d.] c= [.b,b.] ; :: thesis: verum

end;

end;