let p, q, r, s be ext-real number ; :: 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 & q <= s ) by A1, A2, Th50;
then r <= q by A1, XXREAL_0:2;
then r <= s by A3, XXREAL_0:2;
then ( p <= r & s <= q ) by A2, Th50;
hence ( p = r & q = s ) by A3, XXREAL_0:1; :: thesis: verum