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