let p, q, r, s be ExtReal; :: thesis: ( r <= s implies [.r,s.] <> [.p,q.[ )
assume that
A1: r <= s and
A2: [.r,s.] = [.p,q.[ ; :: thesis: contradiction

now :: thesis: not s in [.p,q.[

assume s in [.p,q.[ ; :: thesis: contradiction
then A3: s < q by Th3;
p <= r by A1, A2, Th54;
then p <= s by A1, XXREAL_0:2;
then p < q by A3, XXREAL_0:2;
hence contradiction by A2, A3, Th52; :: thesis: verum

end;

hence contradiction by A1, A2, Th1; :: thesis: verum