let x, y be 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
let n be 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
let e1, e2, e3, e4, e5, e6 be 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
let p1, p2, p3, p4 be Point of (TOP-REAL n); ( e1 = p1 & e2 = p2 & e3 = p3 & e4 = p4 & e5 = p1 + p3 & e6 = p2 + p4 & dist (e1,e2) < x & dist (e3,e4) < y implies dist (e5,e6) < x + y )
assume that
A1:
e1 = p1
and
A2:
e2 = p2
and
A3:
e3 = p3
and
A4:
e4 = p4
and
A5:
e5 = p1 + p3
and
A6:
e6 = p2 + p4
and
A7:
( dist (e1,e2) < x & dist (e3,e4) < y )
; dist (e5,e6) < x + y
reconsider f1 = e1, f2 = e2, f3 = e3, f4 = e4, f5 = e5, f6 = e6 as Element of REAL n by A1, A2, A3, A4, A5, A6, EUCLID:22;
A8:
( |.((f1 - f2) + (f3 - f4)).| <= |.(f1 - f2).| + |.(f3 - f4).| & (dist (e1,e2)) + (dist (e3,e4)) < x + y )
by A7, EUCLID:12, XREAL_1:8;
reconsider u1 = f1, u2 = f2, u3 = f3, u4 = f4, u6 = f6 as Element of n -tuples_on REAL by EUCLID:def 1;
u2 + u4 = u6
by A2, A4, A6;
then A9: (f1 + f3) - f6 =
(u1 - u2) + (u3 - u4)
by Th9
.=
(f1 - f2) + (f3 - f4)
;
A10:
( dist (e1,e2) = |.(f1 - f2).| & dist (e3,e4) = |.(f3 - f4).| )
by SPPOL_1:5;
dist (e5,e6) =
|.(f5 - f6).|
by SPPOL_1:5
.=
|.((f1 - f2) + (f3 - f4)).|
by A1, A3, A5, A9
;
hence
dist (e5,e6) < x + y
by A10, A8, XXREAL_0:2; verum