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

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, Th171
.= ].p,q.[ by A2, A4, Th173 ;
:: thesis: verum

end;

suppose A5: 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 A2, A3, A5, Th178 ;
:: thesis: verum

end;

end;