theorem Th25: :: BKMODEL4:1

for a, b being Real st a <> b holds
1 - (a / (a - b)) = - (b / (a - b))