let p, q be Point of (TOP-REAL 2); for f being V8() 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 V8() 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:8;
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
by CONNSP_1:def 6;
q in A
by RLTOPSP1:68;
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
by CONNSP_1:def 6;
p in A
by RLTOPSP1:68;
then
( A is connected & R meets A )
by A1, A6, CONNSP_1:23, XBOOLE_0:3;
hence
contradiction
by A6, A7, A3, A4, A5, JORDAN2C:92, SPRECT_4:6; verum