let a, b, r1, r2 be Real; :: thesis: ( a <= r1 & r1 <= b & a <= r2 & r2 <= b implies |.(r1 - r2).| <= b - a )

assume that

A1: a <= r1 and

A2: ( r1 <= b & a <= r2 ) and

A3: r2 <= b ; :: thesis: |.(r1 - r2).| <= b - a

assume that

A1: a <= r1 and

A2: ( r1 <= b & a <= r2 ) and

A3: r2 <= b ; :: thesis: |.(r1 - r2).| <= b - a