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;
now :: thesis: 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;
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 )
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;
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 )
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;
end;
end;
hence ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & p1 in C & p2 in C ) ; :: thesis: verum