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

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