let a, b, c, d be real number ; :: thesis: ( a <= b & c <= d & a + c = b + d implies ( a = b & c = d ) )
assume A1: ( a <= b & c <= d & 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, XREAL_1:10; :: thesis: verum