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

per cases ( s <= p or p <= s ) ;

suppose A3: s <= p ; :: thesis: not ].r,s.] c= ].p,q.[

consider t being ext-real number such that
A4: r < t and
A5: t < s by A2, XREAL_1:229;
take t ; :: according to MEMBERED:def 8 :: thesis: ( t in ].r,s.] & not t in ].p,q.[ )
thus t in ].r,s.] by A4, A5, Th2; :: thesis: not t in ].p,q.[
t < p by A3, A5, XXREAL_0:2;
hence not t in ].p,q.[ by Th4; :: thesis: verum

end;

suppose A6: p <= s ; :: thesis: not ].r,s.] c= ].p,q.[

consider t being ext-real number such that
A7: r < t and
A8: t < p by A1, XREAL_1:229;
take t ; :: according to MEMBERED:def 8 :: thesis: ( t in ].r,s.] & not t in ].p,q.[ )
t <= s by A6, A8, XXREAL_0:2;
hence t in ].r,s.] by A7, Th2; :: thesis: not t in ].p,q.[
thus not t in ].p,q.[ by A8, Th4; :: thesis: verum

end;

end;