let p, q, r, s be ExtReal; :: thesis: ( p <= r & r <= s & s <= q implies ([.p,r.] \/ ].r,s.[) \/ [.s,q.] = [.p,q.] )
assume that
A1: p <= r and
A2: r <= s and
A3: s <= q ; :: thesis: ([.p,r.] \/ ].r,s.[) \/ [.s,q.] = [.p,q.]
A4: p <= s by A1, A2, XXREAL_0:2;
A5: r <= q by A2, A3, XXREAL_0:2;

per cases ( r < s or s <= r ) ;

suppose r < s ; :: thesis: ([.p,r.] \/ ].r,s.[) \/ [.s,q.] = [.p,q.]

hence ([.p,r.] \/ ].r,s.[) \/ [.s,q.] = [.p,s.[ \/ [.s,q.] by A1, Th169
.= [.p,q.] by A3, A4, Th166 ;
:: thesis: verum

end;

suppose A6: s <= r ; :: thesis: ([.p,r.] \/ ].r,s.[) \/ [.s,q.] = [.p,q.]

hence ([.p,r.] \/ ].r,s.[) \/ [.s,q.] = ([.p,r.] \/ {}) \/ [.s,q.] by Th28
.= [.p,q.] by A4, A5, A6, Th174 ;
:: thesis: verum

end;

end;