theorem Th14: :: TOPALG_1:14

for p, q, x, y being Real
for n being Nat
for e1, e2, e3, e4, e5, e6 being Point of (Euclid n)
for p1, p2, p3, p4 being Point of (TOP-REAL n) st e1 = p1 & e2 = p2 & e3 = p3 & e4 = p4 & e5 = (x * p1) + (y * p3) & e6 = (x * p2) + (y * p4) & dist (e1,e2) < p & dist (e3,e4) < q & x <> 0 & y <> 0 holds
dist (e5,e6) < (|.x.| * p) + (|.y.| * q)