let p, q be Point of (TOP-REAL 2); :: thesis: 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; :: thesis: ( 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 ; :: 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: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; :: thesis: verum

LSeg (p,q) meets L~ f

let f be V8() standard clockwise_oriented special_circular_sequence; :: thesis: ( 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 ; :: 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: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; :: thesis: verum