let x, y be Real; :: thesis: 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; :: thesis: 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); :: thesis: 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); :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: verum