theorem :: TOPALG_1:12

for 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 = p1 + p3 & e6 = p2 + p4 & dist (e1,e2) < x & dist (e3,e4) < y holds
dist (e5,e6) < x + y