theorem Th06: :: COUSIN2:6

for a, b being Real st a <> 0 holds
a * (b / (2 * a)) = b / 2