let f be rectangular special_circular_sequence; :: thesis: for g being S-Sequence_in_R2 st g /. 1 in LeftComp f & g /. (len g) in RightComp f holds
L~ f meets L~ g
let g be S-Sequence_in_R2; :: thesis: ( g /. 1 in LeftComp f & g /. (len g) in RightComp f implies L~ f meets L~ g )
assume that
A1: g /. 1 in LeftComp f and
A2: g /. (len g) in RightComp f ; :: thesis: L~ f meets L~ g
A3: len g >= 2 by TOPREAL1:def 8;
then g /. 1 in L~ g by JORDAN3:1;
then g /. 1 in (LeftComp f) /\ (L~ g) by A1, XBOOLE_0:def 4;
then A4: LeftComp f meets L~ g ;
g /. (len g) in L~ g by A3, JORDAN3:1;
then g /. (len g) in (RightComp f) /\ (L~ g) by A2, XBOOLE_0:def 4;
then A5: RightComp f meets L~ g ;
A6: LeftComp f misses RightComp f by SPRECT_1:88;
assume L~ f misses L~ g ; :: thesis: contradiction
then L~ g c= (L~ f) ` by SUBSET_1:23;
then A7: L~ g c= (LeftComp f) \/ (RightComp f) by GOBRD12:10;
A8: L~ g is_an_arc_of g /. 1,g /. (len g) by TOPREAL1:25;
A9: RightComp f is open by Th24;
LeftComp f is open by Th24;
hence contradiction by A7, A9, A4, A5, A6, A8, JORDAN6:10, TOPREAL5:1; :: thesis: verum