let y, x be real number ; :: thesis: for n being Nat
for e1, e2, e5, e6 being Point of (Euclid n)
for p1, p2 being Point of (TOP-REAL n) st e1 = p1 & e2 = p2 & e5 = y * p1 & e6 = y * p2 & dist e1,e2 < x & y <> 0 holds
dist e5,e6 < (abs y) * x
let n be Nat; :: thesis: for e1, e2, e5, e6 being Point of (Euclid n)
for p1, p2 being Point of (TOP-REAL n) st e1 = p1 & e2 = p2 & e5 = y * p1 & e6 = y * p2 & dist e1,e2 < x & y <> 0 holds
dist e5,e6 < (abs y) * x
let e1, e2, e5, e6 be Point of (Euclid n); :: thesis: for p1, p2 being Point of (TOP-REAL n) st e1 = p1 & e2 = p2 & e5 = y * p1 & e6 = y * p2 & dist e1,e2 < x & y <> 0 holds
dist e5,e6 < (abs y) * x
let p1, p2 be Point of (TOP-REAL n); :: thesis: ( e1 = p1 & e2 = p2 & e5 = y * p1 & e6 = y * p2 & dist e1,e2 < x & y <> 0 implies dist e5,e6 < (abs y) * x )
assume that
A1: e1 = p1 and
A2: e2 = p2 and
A3: e5 = y * p1 and
A4: e6 = y * p2 and
A5: dist e1,e2 < x and
A6: y <> 0 ; :: thesis: dist e5,e6 < (abs y) * x
reconsider f1 = e1, f2 = e2, f5 = e5, f6 = e6 as Element of REAL n by A1, A2, A3, A4, EUCLID:25;
A7: n in NAT by ORDINAL1:def 13;
then A8: dist e1,e2 = |.(f1 - f2).| by SPPOL_1:20;
A9: 0 < abs y by A6, COMPLEX1:133;
dist e5,e6 = |.(f5 - f6).| by A7, SPPOL_1:20
.= |.((y * f1) - f6).| by A1, A3, EUCLID:69
.= |.((y * f1) - (y * f2)).| by A2, A4, EUCLID:69
.= |.(y * (f1 - f2)).| by Th7
.= (abs y) * |.(f1 - f2).| by EUCLID:14 ;
hence dist e5,e6 < (abs y) * x by A5, A8, A9, XREAL_1:70; :: thesis: verum