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