let p, q, r, s be ExtReal; :: 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 ExtReal such that
A1: u in ].r,s.] and
A2: u in ].p,q.] ;
A3: r < u by A1, Th2;
A4: u <= s by A1, Th2;
A5: p < u by A2, Th2;
u <= q by A2, Th2;
then A6: r <= q by A3, XXREAL_0:2;
A7: p <= s by A4, A5, XXREAL_0:2;
let t be ExtReal; :: 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 A8: t in ].p,q.] \ ].r,s.] ; :: thesis: t in ].p,r.] \/ ].s,q.]
then A9: not t in ].r,s.] by XBOOLE_0:def 5;
A10: p < t by A8, Th2;
A11: t <= q by A8, Th2;
( t <= r or s < t ) by A9, Th2;
then ( t in ].p,r.] or t in ].s,q.] ) by A10, A11, 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 A12: ( ( p < t & t <= r ) or ( s < t & t <= q ) ) by Th2;
then A13: p < t by A7, XXREAL_0:2;
t <= q by A6, A12, XXREAL_0:2;
then A14: t in ].p,q.] by A13, Th2;
not t in ].r,s.] by A12, Th2;
hence t in ].p,q.] \ ].r,s.] by A14, XBOOLE_0:def 5; :: thesis: verum