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
assume L~ f misses L~ g ; :: thesis: contradiction
then L~ g c= (L~ f) ` by SUBSET_1:43;
then A3: L~ g c= (LeftComp f) \/ (RightComp f) by GOBRD12:11;
A4: ( LeftComp f is open & RightComp f is open ) by Th41;
A5: len g >= 2 by TOPREAL1:def 10;
then g /. 1 in L~ g by JORDAN3:34;
then g /. 1 in (LeftComp f) /\ (L~ g) by A1, XBOOLE_0:def 4;
then A6: LeftComp f meets L~ g by XBOOLE_0:4;
g /. (len g) in L~ g by A5, JORDAN3:34;
then g /. (len g) in (RightComp f) /\ (L~ g) by A2, XBOOLE_0:def 4;
then A7: RightComp f meets L~ g by XBOOLE_0:4;
A8: LeftComp f misses RightComp f by SPRECT_1:96;
L~ g is_an_arc_of g /. 1,g /. (len g) by TOPREAL1:31;
hence contradiction by A3, A4, A6, A7, A8, JORDAN6:11, TOPREAL5:4; :: thesis: verum