let a, b, c, d be Real; :: thesis: ( a < b & b < c & c < d implies (REAL \ ].a,d.[) /\ [.b,c.] = {} )
assume A1: ( a < b & b < c & c < d ) ; :: thesis: (REAL \ ].a,d.[) /\ [.b,c.] = {}
thus (REAL \ ].a,d.[) /\ [.b,c.] = (].-infty,a.] \/ [.d,+infty.[) /\ [.b,c.] by XXREAL_1:398
.= (].-infty,a.] /\ [.b,c.]) \/ ([.d,+infty.[ /\ [.b,c.]) by XBOOLE_1:23
.= {} \/ ([.d,+infty.[ /\ [.b,c.]) by XBOOLE_0:def 7, XXREAL_1:280, A1
.= {} by XBOOLE_0:def 7, XXREAL_1:277, A1 ; :: thesis: verum