theorem Th14: :: BAGORD_2:5

for k, x1, x2, y1, y2 being Nat st x2 <= k & x1 <= (k -' x2) + y2 holds
( x2 + (x1 -' y2) <= k & (((k -' x2) + y2) -' x1) + y1 = (k -' (x2 + (x1 -' y2))) + ((y2 -' x1) + y1) )