theorem Th29: :: SURREALI:29

for x, x1, x2, y1, y2 being Surreal holds
( ((1_No + ((x2 - x) * y2)) * x1) + (- ((1_No + ((x1 - x) * y1)) * x2)) == ((x1 - x2) * (1_No - (x * y1))) + (((y1 - y2) * x1) * (x - x2)) & ((1_No + ((x2 - x) * y2)) * x1) - ((1_No + ((x1 - x) * y1)) * x2) == ((x1 - x2) * (1_No - (x * y2))) + (((y2 - y1) * x2) * (x1 - x)) )