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) )
reconsider k = (max (a,b)) - (max (c,d)) as Real ;
A2: k = (min (c,d)) - (min (a,b)) by A1, SAD;
A3: ( max (a,b) > max (c,d) implies min (a,b) < min (c,d) )
proof
assume max (a,b) > max (c,d) ; :: thesis: min (a,b) < min (c,d)
then (max (a,b)) - (max (c,d)) > (max (c,d)) - (max (c,d)) by XREAL_1:9;
then k + (min (a,b)) > 0 + (min (a,b)) by XREAL_1:6;
hence min (a,b) < min (c,d) by A2; :: thesis: verum
end;
( max (a,b) <= max (c,d) implies min (a,b) >= min (c,d) )
proof
assume max (a,b) <= max (c,d) ; :: thesis: min (a,b) >= min (c,d)
then (max (a,b)) - (max (c,d)) <= (max (c,d)) - (max (c,d)) by XREAL_1:9;
then k + (min (a,b)) <= 0 + (min (a,b)) by XREAL_1:6;
hence min (a,b) >= min (c,d) by A2; :: thesis: verum
end;
hence ( max (a,b) > max (c,d) iff min (a,b) < min (c,d) ) by A3; :: thesis: verum