let f be non constant standard special_circular_sequence; :: thesis: for p1, p2 being Point of (TOP-REAL 2) st LSeg (p1,p2) misses L~ f holds

ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & p1 in C & p2 in C )

let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( LSeg (p1,p2) misses L~ f implies ex C being Subset of (TOP-REAL 2) 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 (TOP-REAL 2) 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 A1, XBOOLE_0:3;

A5: p2 in LSeg (p1,p2) by RLTOPSP1:68;

then A6: not p2 in L~ f by A1, XBOOLE_0:3;

A7: ( not p2 in RightComp f or not p1 in LeftComp f ) by A1, A3, A5, JORDAN1J:36;

A8: LeftComp f is_a_component_of (L~ f) ` by GOBOARD9:def 1;

( C is_a_component_of (L~ f) ` & p1 in C & p2 in C ) ; :: thesis: verum

ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & p1 in C & p2 in C )

let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( LSeg (p1,p2) misses L~ f implies ex C being Subset of (TOP-REAL 2) 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 (TOP-REAL 2) 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 A1, XBOOLE_0:3;

A5: p2 in LSeg (p1,p2) by RLTOPSP1:68;

then A6: not p2 in L~ f by A1, XBOOLE_0:3;

A7: ( not p2 in RightComp f or not p1 in LeftComp f ) by A1, A3, A5, JORDAN1J:36;

A8: LeftComp f is_a_component_of (L~ f) ` by GOBOARD9:def 1;

now :: thesis: ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & p1 in C & p2 in C )end;

hence
ex C being Subset of (TOP-REAL 2) 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 A1, A3, A5, JORDAN1J:36;

end;

suppose
not p1 in RightComp f
; :: thesis: ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & p1 in C & p2 in C )

( C is_a_component_of (L~ f) ` & p1 in C & p2 in C )

then
( p1 in LeftComp f & p2 in LeftComp f )
by A7, A4, A6, GOBRD14:17;

hence ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & p1 in C & p2 in C ) by A8; :: thesis: verum

end;hence ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & p1 in C & p2 in C ) by A8; :: thesis: verum

suppose
not p2 in LeftComp f
; :: thesis: ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & p1 in C & p2 in C )

( C is_a_component_of (L~ f) ` & p1 in C & p2 in C )

then
( p2 in RightComp f & p1 in RightComp f )
by A7, A4, A6, GOBRD14:18;

hence ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & p1 in C & p2 in C ) by A2; :: thesis: verum

end;hence ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & p1 in C & p2 in C ) by A2; :: thesis: verum

( C is_a_component_of (L~ f) ` & p1 in C & p2 in C ) ; :: thesis: verum