theorem Th35:
for
n being
Nat for
a being
Real for
Q being
Subset of
(TOP-REAL n) for
w1,
w7 being
Point of
(TOP-REAL n) st
n >= 2 &
Q = { q where q is Point of (TOP-REAL n) : |.q.| > a } &
w1 in Q &
w7 in Q & ex
r being
Real st
(
w1 = r * w7 or
w7 = r * w1 ) holds
ex
w2,
w3,
w4,
w5,
w6 being
Point of
(TOP-REAL n) st
(
w2 in Q &
w3 in Q &
w4 in Q &
w5 in Q &
w6 in Q &
LSeg (
w1,
w2)
c= Q &
LSeg (
w2,
w3)
c= Q &
LSeg (
w3,
w4)
c= Q &
LSeg (
w4,
w5)
c= Q &
LSeg (
w5,
w6)
c= Q &
LSeg (
w6,
w7)
c= Q )