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
A3: not r in ].r,s.] by Th2;
A4: p <= r by A1, A2, Th57;
s <= q by A1, A2, Th57;
then r < q by A1, XXREAL_0:2;
hence contradiction by A2, A3, A4, Th3; :: thesis: verum