theorem Th50:
for
f being
constant standard special_circular_sequence for
i1,
i2 being
Nat st 1
<= i1 &
i1 + 1
<= len f & 1
<= i2 &
i2 + 1
<= len f &
i1 <> i2 holds
ex
g1,
g2 being
FinSequence of
(TOP-REAL 2) st
(
g1 is_a_part_of f,
i1,
i2 &
g2 is_a_part_of f,
i1,
i2 &
(L~ g1) /\ (L~ g2) = {(f . i1),(f . i2)} &
(L~ g1) \/ (L~ g2) = L~ f &
L~ g1 is_S-P_arc_joining f /. i1,
f /. i2 &
L~ g2 is_S-P_arc_joining f /. i1,
f /. i2 & ( for
g being
FinSequence of
(TOP-REAL 2) holds
( not
g is_a_part_of f,
i1,
i2 or
g = g1 or
g = g2 ) ) )