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

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