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

per cases ( r <= q or q < r ) ;

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

consider t being ExtReal such that
A4: q < t and
A5: t < s by A1, XREAL_1:227;
take t ; :: according to MEMBERED:def 8 :: thesis: ( t in [.r,s.] & not t in [.p,q.] )
r < t by A3, A4, XXREAL_0:2;
hence t in [.r,s.] by A5, Th1; :: thesis: not t in [.p,q.]
thus not t in [.p,q.] by A4, Th1; :: thesis: verum

end;

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

take t = r; :: according to MEMBERED:def 8 :: thesis: ( t in [.r,s.] & not t in [.p,q.] )
thus t in [.r,s.] by A2, Th1; :: thesis: not t in [.p,q.]
thus not t in [.p,q.] by A6, Th1; :: thesis: verum

end;

end;