let p, q be ext-real number ; :: thesis: ( p <= q implies ].q,p.] = {} )
assume A1: p <= q ; :: thesis: ].q,p.] = {}
assume ].q,p.] <> {} ; :: thesis: contradiction
then consider r being ext-real number such that
A2: r in ].q,p.] by MEMBERED:8;
( q < r & r <= p ) by A2, Th2;
hence contradiction by A1, XXREAL_0:2; :: thesis: verum