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