let a, b, c, d be positive Real; :: thesis: ( max (a,b) = max (c,d) & min (a,b) = min (c,d) iff ( a * b = c * d & a + b = c + d ) )
A1: ( a + b = (max (a,b)) + (min (a,b)) & c + d = (max (c,d)) + (min (c,d)) & a * b = (max (a,b)) * (min (a,b)) & (max (c,d)) * (min (c,d)) = c * d ) by NEWTON04:18;
( a * b = c * d & a + b = c + d implies ( max (a,b) = max (c,d) & min (a,b) = min (c,d) ) )

proof

assume B1: ( a * b = c * d & a + b = c + d ) ; :: thesis: ( max (a,b) = max (c,d) & min (a,b) = min (c,d) )
then max (a,b) = max (c,d) by ISM;
hence ( max (a,b) = max (c,d) & min (a,b) = min (c,d) ) by A1, B1; :: thesis: verum

end;

hence ( max (a,b) = max (c,d) & min (a,b) = min (c,d) iff ( a * b = c * d & a + b = c + d ) ) by A1; :: thesis: verum