let a, b, c, d be Real; ( a <= b & c <= d & a + c = b + d implies ( a = b & c = d ) )
assume that
A1:
( a <= b & c <= d )
and
A2:
a + c = b + d
; ( a = b & c = d )
assume
( not a = b or not c = d )
; contradiction
then
( a < b or c < d )
by A1, XXREAL_0:1;
hence
contradiction
by A1, A2, XREAL_1:8; verum