let a, b, c, d be positive Real; :: thesis: ( a + b = c + d implies ( max (a,b) = max (c,d) iff min (a,b) = min (c,d) ) )
assume A1: a + b = c + d ; :: thesis: ( max (a,b) = max (c,d) iff min (a,b) = min (c,d) )
( ( ( max (a,b) = a & min (a,b) = b ) or ( max (a,b) = b & min (a,b) = a ) ) & ( ( max (c,d) = c & min (c,d) = d ) or ( max (c,d) = d & min (c,d) = c ) ) ) by XXREAL_0:def 9, XXREAL_0:def 10;
hence ( max (a,b) = max (c,d) iff min (a,b) = min (c,d) ) by A1; :: thesis: verum