let p, p1, p2 be Point of (TOP-REAL 2); :: thesis: for f being non constant standard special_circular_sequence st (L~ f) /\ (LSeg (p1,p2)) = {p} holds
for r being Point of (TOP-REAL 2) st not r in LSeg (p1,p2) & not p1 in L~ f & not p2 in L~ f & ( ( p1 `1 = p2 `1 & p1 `1 = r `1 ) or ( p1 `2 = p2 `2 & p1 `2 = r `2 ) ) & ex i being Nat st
( 1 <= i & i + 1 <= len f & ( r in right_cell (f,i,(GoB f)) or r in left_cell (f,i,(GoB f)) ) & p in LSeg (f,i) ) & not r in L~ f & ( for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not r in C or not p1 in C ) ) holds
ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C )
let f be non constant standard special_circular_sequence; :: thesis: ( (L~ f) /\ (LSeg (p1,p2)) = {p} implies for r being Point of (TOP-REAL 2) st not r in LSeg (p1,p2) & not p1 in L~ f & not p2 in L~ f & ( ( p1 `1 = p2 `1 & p1 `1 = r `1 ) or ( p1 `2 = p2 `2 & p1 `2 = r `2 ) ) & ex i being Nat st
( 1 <= i & i + 1 <= len f & ( r in right_cell (f,i,(GoB f)) or r in left_cell (f,i,(GoB f)) ) & p in LSeg (f,i) ) & not r in L~ f & ( for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not r in C or not p1 in C ) ) holds
ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C ) )
assume (L~ f) /\ (LSeg (p1,p2)) = {p} ; :: thesis: for r being Point of (TOP-REAL 2) st not r in LSeg (p1,p2) & not p1 in L~ f & not p2 in L~ f & ( ( p1 `1 = p2 `1 & p1 `1 = r `1 ) or ( p1 `2 = p2 `2 & p1 `2 = r `2 ) ) & ex i being Nat st
( 1 <= i & i + 1 <= len f & ( r in right_cell (f,i,(GoB f)) or r in left_cell (f,i,(GoB f)) ) & p in LSeg (f,i) ) & not r in L~ f & ( for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not r in C or not p1 in C ) ) holds
ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C )
then A1: p in (L~ f) /\ (LSeg (p1,p2)) by TARSKI:def 1;
then A2: p in LSeg (p1,p2) by XBOOLE_0:def 4;
let r be Point of (TOP-REAL 2); :: thesis: ( not r in LSeg (p1,p2) & not p1 in L~ f & not p2 in L~ f & ( ( p1 `1 = p2 `1 & p1 `1 = r `1 ) or ( p1 `2 = p2 `2 & p1 `2 = r `2 ) ) & ex i being Nat st
( 1 <= i & i + 1 <= len f & ( r in right_cell (f,i,(GoB f)) or r in left_cell (f,i,(GoB f)) ) & p in LSeg (f,i) ) & not r in L~ f & ( for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not r in C or not p1 in C ) ) implies ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C ) )
assume that
A3: not r in LSeg (p1,p2) and
A4: not p1 in L~ f and
A5: not p2 in L~ f and
A6: ( ( p1 `1 = p2 `1 & p1 `1 = r `1 ) or ( p1 `2 = p2 `2 & p1 `2 = r `2 ) ) and
A7: ex i being Nat st
( 1 <= i & i + 1 <= len f & ( r in right_cell (f,i,(GoB f)) or r in left_cell (f,i,(GoB f)) ) & p in LSeg (f,i) ) and
A8: not r in L~ f ; :: thesis: ( ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p1 in C ) or ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C ) )
consider i being Nat such that
A9: ( 1 <= i & i + 1 <= len f ) and
A10: ( r in right_cell (f,i,(GoB f)) or r in left_cell (f,i,(GoB f)) ) and
A11: p in LSeg (f,i) by A7;
A12: right_cell (f,i,(GoB f)) is convex by A9, Th22;
A13: f is_sequence_on GoB f by GOBOARD5:def 5;
then A14: (right_cell (f,i,(GoB f))) \ (L~ f) c= RightComp f by A9, JORDAN9:27;
A15: now :: thesis: ( r in right_cell (f,i,(GoB f)) implies r in RightComp f )
assume r in right_cell (f,i,(GoB f)) ; :: thesis: r in RightComp f
then r in (right_cell (f,i,(GoB f))) \ (L~ f) by A8, XBOOLE_0:def 5;
hence r in RightComp f by A14; :: thesis: verum
end;
A16: LSeg (f,i) c= right_cell (f,i,(GoB f)) by A13, A9, JORDAN1H:22;
A17: now :: thesis: ( p1 in LSeg (r,p) & r in right_cell (f,i,(GoB f)) implies ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p1 in C ) )
assume that
A18: p1 in LSeg (r,p) and
A19: r in right_cell (f,i,(GoB f)) ; :: thesis: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p1 in C )
LSeg (r,p) c= right_cell (f,i,(GoB f)) by A11, A16, A12, A19;
then p1 in (right_cell (f,i,(GoB f))) \ (L~ f) by A4, A18, XBOOLE_0:def 5;
hence ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p1 in C ) by A14, A15, A19, Th14; :: thesis: verum
end;
A20: left_cell (f,i,(GoB f)) is convex by A9, Th22;
A21: (left_cell (f,i,(GoB f))) \ (L~ f) c= LeftComp f by A13, A9, JORDAN9:27;
A22: now :: thesis: ( r in left_cell (f,i,(GoB f)) implies r in LeftComp f )
assume r in left_cell (f,i,(GoB f)) ; :: thesis: r in LeftComp f
then r in (left_cell (f,i,(GoB f))) \ (L~ f) by A8, XBOOLE_0:def 5;
hence r in LeftComp f by A21; :: thesis: verum
end;
A23: LSeg (f,i) c= left_cell (f,i,(GoB f)) by A13, A9, JORDAN1H:20;
A24: now :: thesis: ( p1 in LSeg (r,p) & r in left_cell (f,i,(GoB f)) implies ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p1 in C ) )
assume that
A25: p1 in LSeg (r,p) and
A26: r in left_cell (f,i,(GoB f)) ; :: thesis: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p1 in C )
LSeg (r,p) c= left_cell (f,i,(GoB f)) by A11, A23, A20, A26;
then p1 in (left_cell (f,i,(GoB f))) \ (L~ f) by A4, A25, XBOOLE_0:def 5;
hence ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p1 in C ) by A21, A22, A26, Th14; :: thesis: verum
end;
A27: now :: thesis: ( p2 in LSeg (r,p) & r in left_cell (f,i,(GoB f)) implies ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C ) )
assume that
A28: p2 in LSeg (r,p) and
A29: r in left_cell (f,i,(GoB f)) ; :: thesis: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C )
LSeg (r,p) c= left_cell (f,i,(GoB f)) by A11, A23, A20, A29;
then p2 in (left_cell (f,i,(GoB f))) \ (L~ f) by A5, A28, XBOOLE_0:def 5;
hence ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C ) by A21, A22, A29, Th14; :: thesis: verum
end;
A30: now :: thesis: ( p2 in LSeg (r,p) & r in right_cell (f,i,(GoB f)) implies ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C ) )
assume that
A31: p2 in LSeg (r,p) and
A32: r in right_cell (f,i,(GoB f)) ; :: thesis: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C )
LSeg (r,p) c= right_cell (f,i,(GoB f)) by A11, A16, A12, A32;
then p2 in (right_cell (f,i,(GoB f))) \ (L~ f) by A5, A31, XBOOLE_0:def 5;
hence ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C ) by A14, A15, A32, Th14; :: thesis: verum
end;
A33: ( p <> p2 & p <> p1 ) by A4, A5, A1, XBOOLE_0:def 4;
per cases ( p1 in LSeg (r,p) or p2 in LSeg (r,p) ) by A3, A6, A33, A2, Th28;
suppose A34: p1 in LSeg (r,p) ; :: thesis: ( ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p1 in C ) or ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C ) )
now :: thesis: ( ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p1 in C ) or ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C ) )
per cases ( r in right_cell (f,i,(GoB f)) or r in left_cell (f,i,(GoB f)) ) by A10;
suppose r in right_cell (f,i,(GoB f)) ; :: thesis: ( ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p1 in C ) or ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C ) )
hence ( ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p1 in C ) or ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C ) ) by A17, A34; :: thesis: verum
end;
suppose r in left_cell (f,i,(GoB f)) ; :: thesis: ( ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p1 in C ) or ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C ) )
hence ( ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p1 in C ) or ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C ) ) by A24, A34; :: thesis: verum
end;
end;
end;
hence ( ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p1 in C ) or ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C ) ) ; :: thesis: verum
end;
suppose A35: p2 in LSeg (r,p) ; :: thesis: ( ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p1 in C ) or ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C ) )
now :: thesis: ( ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p1 in C ) or ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C ) )
per cases ( r in right_cell (f,i,(GoB f)) or r in left_cell (f,i,(GoB f)) ) by A10;
suppose r in right_cell (f,i,(GoB f)) ; :: thesis: ( ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p1 in C ) or ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C ) )
hence ( ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p1 in C ) or ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C ) ) by A30, A35; :: thesis: verum
end;
suppose r in left_cell (f,i,(GoB f)) ; :: thesis: ( ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p1 in C ) or ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C ) )
hence ( ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p1 in C ) or ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C ) ) by A27, A35; :: thesis: verum
end;
end;
end;
hence ( ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p1 in C ) or ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C ) ) ; :: thesis: verum
end;
end;