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