let p, q, r, s be ExtReal; :: thesis: ( p < q & [.p,q.[ = [.r,s.[ implies ( p = r & q = s ) )
assume that
A1: p < q and
A2: [.p,q.[ = [.r,s.[ ; :: thesis: ( p = r & q = s )
A3: r <= p by A1, A2, Th55;
A4: q <= s by A1, A2, Th55;
r < q by A1, A3, XXREAL_0:2;
then A5: r < s by A4, XXREAL_0:2;
then A6: p <= r by A2, Th55;
s <= q by A2, A5, Th55;
hence ( p = r & q = s ) by A3, A4, A6, XXREAL_0:1; :: thesis: verum