theorem Th1: :: INTEGRA6:1

for a, b, c, d being Real st a <= b & c <= d & a + c = b + d holds
( a = b & c = d )