theorem :: FUZZY_9:7

for p, q, s, t being Real st s <> p holds
( (AffineMap (p,q)) . ((t - q) / (p - s)) = (AffineMap (s,t)) . ((t - q) / (p - s)) & (AffineMap (s,t)) . ((t - q) / (p - s)) = ((p * t) - (q * s)) / (p - s) )