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, Th50;
A4: q <= s by A1, A2, Th50;
r <= q by A1, A3, XXREAL_0:2;
then A5: r <= s by A4, XXREAL_0:2;
then A6: p <= r by A2, Th50;
s <= q by A2, A5, Th50;
hence ( p = r & q = s ) by A3, A4, A6, XXREAL_0:1; :: thesis: verum