let a, b, c, d be Real; :: thesis:
assume A1: b <= c ; :: thesis:

per cases ;

suppose A2: a <= b ; :: thesis:

per cases ;

suppose c <= d ; :: thesis:

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:

end;

suppose d < c ; :: thesis:

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

end;

end;

end;

suppose b < a ; :: thesis:

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

end;

end;