let f be non constant standard special_circular_sequence; :: thesis: for p1, p2 being Point of () st LSeg (p1,p2) misses L~ f holds
ex C being Subset of () st
( C is_a_component_of (L~ f) ` & p1 in C & p2 in C )

let p1, p2 be Point of (); :: thesis: ( LSeg (p1,p2) misses L~ f implies ex C being Subset of () st
( C is_a_component_of (L~ f) ` & p1 in C & p2 in C ) )

assume A1: LSeg (p1,p2) misses L~ f ; :: thesis: ex C being Subset of () st
( C is_a_component_of (L~ f) ` & p1 in C & p2 in C )

A2: RightComp f is_a_component_of (L~ f) ` by GOBOARD9:def 2;
A3: p1 in LSeg (p1,p2) by RLTOPSP1:68;
then A4: not p1 in L~ f by ;
A5: p2 in LSeg (p1,p2) by RLTOPSP1:68;
then A6: not p2 in L~ f by ;
A7: ( not p2 in RightComp f or not p1 in LeftComp f ) by ;
A8: LeftComp f is_a_component_of (L~ f) ` by GOBOARD9:def 1;
now :: thesis: ex C being Subset of () st
( C is_a_component_of (L~ f) ` & p1 in C & p2 in C )
per cases ( not p1 in RightComp f or not p2 in LeftComp f ) by ;
suppose not p1 in RightComp f ; :: thesis: ex C being Subset of () st
( C is_a_component_of (L~ f) ` & p1 in C & p2 in C )

then ( p1 in LeftComp f & p2 in LeftComp f ) by ;
hence ex C being Subset of () st
( C is_a_component_of (L~ f) ` & p1 in C & p2 in C ) by A8; :: thesis: verum
end;
suppose not p2 in LeftComp f ; :: thesis: ex C being Subset of () st
( C is_a_component_of (L~ f) ` & p1 in C & p2 in C )

then ( p2 in RightComp f & p1 in RightComp f ) by ;
hence ex C being Subset of () st
( C is_a_component_of (L~ f) ` & p1 in C & p2 in C ) by A2; :: thesis: verum
end;
end;
end;
hence ex C being Subset of () st
( C is_a_component_of (L~ f) ` & p1 in C & p2 in C ) ; :: thesis: verum