theorem Th61: :: TOPGEN_5:61
for x, y being Real
for r being positive Real st x <> y holds
(+ (x,r)) . |[y,0]| = 1