let p, q, r, s be ExtReal; :: thesis: [.r,s.[ \/ [.p,q.[ c= [.(min (r,p)),(max (s,q)).[
let t be ExtReal; :: according to MEMBERED:def 8 :: thesis: ( not t in [.r,s.[ \/ [.p,q.[ or t in [.(min (r,p)),(max (s,q)).[ )
assume t in [.r,s.[ \/ [.p,q.[ ; :: thesis: t in [.(min (r,p)),(max (s,q)).[
then ( t in [.r,s.[ or t in [.p,q.[ ) by XBOOLE_0:def 3;
then A1: ( ( r <= t & t < s ) or ( p <= t & t < q ) ) by Th3;
then A2: min (r,p) <= t by XXREAL_0:23;
t < max (s,q) by A1, XXREAL_0:30;
hence t in [.(min (r,p)),(max (s,q)).[ by A2, Th3; :: thesis: verum