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