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, Th2;
r <= p by A2, Th2;
hence contradiction by A1, A3, XXREAL_0:2; :: thesis: verum