let r, s, p, q be ext-real number ; :: thesis: [.r,s.[ \/ [.p,q.[ c= [.(min r,p),(max s,q).[
let t be ext-real number ; :: 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