theorem Th36: :: SPPOL_2:36

for f, g being FinSequence of (TOP-REAL 2) st f is s.n.c. & g is s.n.c. & L~ f misses L~ g & ( for i being Nat st 1 <= i & i + 2 <= len f holds
LSeg (f,i) misses LSeg ((f /. (len f)),(g /. 1)) ) & ( for i being Nat st 2 <= i & i + 1 <= len g holds
LSeg (g,i) misses LSeg ((f /. (len f)),(g /. 1)) ) holds
f ^ g is s.n.c.