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