let a, b, c, d be positive Real; :: thesis: ( a + b = c + d implies (max (a,b)) - (max (c,d)) = (min (c,d)) - (min (a,b)) )
assume A1: a + b = c + d ; :: thesis: (max (a,b)) - (max (c,d)) = (min (c,d)) - (min (a,b))
( ( ( 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)) = (min (c,d)) - (min (a,b)) by A1; :: thesis: verum