let p, q be Point of (TOP-REAL 2); :: thesis: for f being non constant standard clockwise_oriented special_circular_sequence st p in RightComp f & q in LeftComp f holds
LSeg p,q meets L~ f
let f be non constant standard clockwise_oriented special_circular_sequence; :: thesis: ( p in RightComp f & q in LeftComp f implies LSeg p,q meets L~ f )
assume A1: ( p in RightComp f & q in LeftComp f ) ; :: thesis: LSeg p,q meets L~ f
assume LSeg p,q misses L~ f ; :: thesis: contradiction
then LSeg p,q c= (L~ f) ` by TDLAT_1:2;
then reconsider A = LSeg p,q as Subset of ((TOP-REAL 2) | ((L~ f) ` )) by PRE_TOPC:29;
A2: A is connected by CONNSP_1:24;
RightComp f is_a_component_of (L~ f) ` by GOBOARD9:def 2;
then consider R being Subset of ((TOP-REAL 2) | ((L~ f) ` )) such that
A3: R = RightComp f and
A4: R is_a_component_of (TOP-REAL 2) | ((L~ f) ` ) by CONNSP_1:def 6;
LeftComp f is_a_component_of (L~ f) ` by GOBOARD9:def 1;
then consider L being Subset of ((TOP-REAL 2) | ((L~ f) ` )) such that
A5: L = LeftComp f and
A6: L is_a_component_of (TOP-REAL 2) | ((L~ f) ` ) by CONNSP_1:def 6;
( p in A & q in A ) by RLTOPSP1:69;
then ( R meets A & L meets A ) by A1, A3, A5, XBOOLE_0:3;
hence contradiction by A2, A3, A4, A5, A6, JORDAN2C:100, SPRECT_4:7; :: thesis: verum