let p, q be ext-real number ; :: thesis: ( p < q implies not ].p,q.[ is empty )
assume p < q ; :: thesis: not ].p,q.[ is empty
then ex s being ext-real number st
( p < s & s < q ) by XREAL_1:229;
hence not ].p,q.[ is empty by Th4; :: thesis: verum