theorem Th17L: :: FUZZY_6:28

for a, b, p, q being Real
for f being Function of REAL,REAL st a <> p & f = ((AffineMap (a,b)) | ].-infty,((q - b) / (a - p)).[) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),+infty.[) holds
f is Lipschitzian