let p, q be Point of (TOP-REAL 2); 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; ( p in RightComp f & q in LeftComp f implies LSeg p,q meets L~ f )
assume that
A1:
p in RightComp f
and
A2:
q in LeftComp f
; LSeg p,q meets L~ f
assume
LSeg p,q misses L~ f
; 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;
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
A3:
L = LeftComp f
and
A4:
L is_a_component_of (TOP-REAL 2) | ((L~ f) ` )
by CONNSP_1:def 6;
q in A
by RLTOPSP1:69;
then A5:
L meets A
by A2, A3, XBOOLE_0:3;
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
A6:
R = RightComp f
and
A7:
R is_a_component_of (TOP-REAL 2) | ((L~ f) ` )
by CONNSP_1:def 6;
p in A
by RLTOPSP1:69;
then
( A is connected & R meets A )
by A1, A6, CONNSP_1:24, XBOOLE_0:3;
hence
contradiction
by A6, A7, A3, A4, A5, JORDAN2C:100, SPRECT_4:7; verum