let x, y be real number ; :: thesis: for n being Element of 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 Element of 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 & e2 = p2 & e3 = p3 & e4 = p4 ) and
A2: e5 = p1 + p3 and
A3: e6 = p2 + p4 and
A4: dist e1,e2 < x and
A5: dist e3,e4 < y ; :: thesis: dist e5,e6 < x + y
reconsider f1 = e1, f2 = e2, f3 = e3, f4 = e4, f6 = e6 as Element of REAL n by A1, A3, EUCLID:25;
A6: REAL n = n -tuples_on REAL by EUCLID:def 1;
A7: dist e5,e6 = |.((f1 + f3) - f6).| by A1, A2, SPPOL_1:20
.= |.((f1 - f2) + (f3 - f4)).| by A1, A3, A6, Th9 ;
A8: ( dist e1,e2 = |.(f1 - f2).| & dist e3,e4 = |.(f3 - f4).| ) by SPPOL_1:20;
A9: |.((f1 - f2) + (f3 - f4)).| <= |.(f1 - f2).| + |.(f3 - f4).| by EUCLID:15;
(dist e1,e2) + (dist e3,e4) < x + y by A4, A5, XREAL_1:10;
hence dist e5,e6 < x + y by A7, A8, A9, XXREAL_0:2; :: thesis: verum