let a, b, c, d be Real; :: thesis: ( 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 ; :: thesis: ( a = b & c = d )
assume ( not a = b or not c = d ) ; :: thesis: contradiction
then ( a < b or c < d ) by A1, XXREAL_0:1;
hence contradiction by A1, A2, XREAL_1:8; :: thesis: verum