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