let p, q be ExtReal; :: thesis: ( p < q implies [.q,p.] = {} )
assume A1: p < q ; :: thesis: [.q,p.] = {}
assume [.q,p.] <> {} ; :: thesis: contradiction
then consider r being ExtReal such that
A2: r in [.q,p.] ;
A3: q <= r by A2, Th1;
r <= p by A2, Th1;
hence contradiction by A1, A3, XXREAL_0:2; :: thesis: verum