let p, q, r, s be ext-real number ; :: thesis: ( ].p,q.] meets ].r,s.] implies ].p,q.] \ ].r,s.] = ].p,r.] \/ ].s,q.] )
assume ].p,q.] meets ].r,s.] ; :: thesis: ].p,q.] \ ].r,s.] = ].p,r.] \/ ].s,q.]
then consider u being ext-real number such that
A1: u in ].r,s.] and
A2: u in ].p,q.] by MEMBERED:def 20;
A3: ( r < u & u <= s ) by A1, Th2;
A4: ( p < u & u <= q ) by A2, Th2;
then A5: r <= q by A3, XXREAL_0:2;
A6: p <= s by A3, A4, XXREAL_0:2;
let t be ext-real number ; :: according to MEMBERED:def 14 :: thesis: ( ( not t in ].p,q.] \ ].r,s.] or t in ].p,r.] \/ ].s,q.] ) & ( not t in ].p,r.] \/ ].s,q.] or t in ].p,q.] \ ].r,s.] ) )
thus ( t in ].p,q.] \ ].r,s.] implies t in ].p,r.] \/ ].s,q.] ) :: thesis: ( not t in ].p,r.] \/ ].s,q.] or t in ].p,q.] \ ].r,s.] )

proof

assume t in ].p,q.] \ ].r,s.] ; :: thesis: t in ].p,r.] \/ ].s,q.]
then ( t in ].p,q.] & not t in ].r,s.] ) by XBOOLE_0:def 5;
then ( p < t & t <= q & ( t <= r or s < t ) ) by Th2;
then ( t in ].p,r.] or t in ].s,q.] ) by Th2;
hence t in ].p,r.] \/ ].s,q.] by XBOOLE_0:def 3; :: thesis: verum

end;

assume t in ].p,r.] \/ ].s,q.] ; :: thesis: t in ].p,q.] \ ].r,s.]
then ( t in ].p,r.] or t in ].s,q.] ) by XBOOLE_0:def 3;
then ( ( p < t & t <= r ) or ( s < t & t <= q ) ) by Th2;
then ( p < t & t <= q & ( t <= r or s < t ) ) by A5, A6, XXREAL_0:2;
then ( t in ].p,q.] & not t in ].r,s.] ) by Th2;
hence t in ].p,q.] \ ].r,s.] by XBOOLE_0:def 5; :: thesis: verum