theorem Th17E: :: FUZZY_6:30

for a, b, p, q being Real st a <> p holds
(AffineMap (a,b)) . ((q - b) / (a - p)) = (AffineMap (p,q)) . ((q - b) / (a - p))