let q, s, r, p be ext-real number ; :: 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.[
take t = s; :: according to MEMBERED:def 8 :: thesis: ( t in ].r,s.] & not t in [.p,q.[ )
thus t in ].r,s.] by A2, Th2; :: thesis: not t in [.p,q.[
thus not t in [.p,q.[ by A1, Th3; :: thesis: verum