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

now :: thesis: for t being ExtReal st r < t & t < s holds
p <= t

let t be ExtReal; :: thesis: ( r < t & t < s implies p <= t )
assume that
A3: r < t and
A4: t < s ; :: thesis: p <= t
t in ].r,s.[ by A3, A4, Th4;
hence p <= t by A2, Th1; :: thesis: verum

end;

hence p <= r by A1, XREAL_1:228; :: thesis: s <= q

now :: thesis: for t being ExtReal st r < t & t < s holds
t <= q

let t be ExtReal; :: thesis: ( r < t & t < s implies t <= q )
assume that
A5: r < t and
A6: t < s ; :: thesis: t <= q
t in ].r,s.[ by A5, A6, Th4;
hence t <= q by A2, Th1; :: thesis: verum

end;

hence s <= q by A1, XREAL_1:229; :: thesis: verum