let f be non constant standard special_circular_sequence; :: thesis:
let g be special FinSequence of (TOP-REAL 2); :: thesis:
assume A1: f,g are_in_general_position ; :: thesis:
A2: g is_in_general_position_wrt f by A1;
let k be Nat; :: thesis:
assume that
A3: 1 <= k and
A4: k + 1 <= len g ; :: thesis:
A5: g . k in (L~ f) ` by A1, A3, A4, Th8;
then A6: not g . k in L~ f by XBOOLE_0:def 5;
A7: g . (k + 1) in (L~ f) ` by A1, A3, A4, Th8;
then A8: not g . (k + 1) in L~ f by XBOOLE_0:def 5;
A9: k < len g by A4, NAT_1:13;
then A10: k in dom g by A3, FINSEQ_3:25;
then A11: g /. k = g . k by PARTFUN1:def 6;
then A12: g . k in LSeg (g,k) by A3, A4, TOPREAL1:21;
set m = (L~ f) /\ (LSeg (g,k));
set p1 = g /. k;
set p2 = g /. (k + 1);
A13: LSeg (g,k) = LSeg ((g /. k),(g /. (k + 1))) by A3, A4, TOPREAL1:def 3;
( LSeg (g,k) is vertical or LSeg (g,k) is horizontal ) by SPPOL_1:19;
then A14: ( (g /. k) `1 = (g /. (k + 1)) `1 or (g /. k) `2 = (g /. (k + 1)) `2 ) by A13, SPPOL_1:15, SPPOL_1:16;
A15: rng g c= the carrier of (TOP-REAL 2) by FINSEQ_1:def 4;
1 <= k + 1 by A3, NAT_1:13;
then A16: k + 1 in dom g by A4, FINSEQ_3:25;
then A17: g /. (k + 1) = g . (k + 1) by PARTFUN1:def 6;
then A18: g . (k + 1) in LSeg (g,k) by A3, A4, TOPREAL1:21;
g . (k + 1) in rng g by A16, FUNCT_1:3;
then reconsider gk1 = g . (k + 1) as Point of (TOP-REAL 2) by A15;
g . k in rng g by A10, FUNCT_1:3;
then reconsider gk = g . k as Point of (TOP-REAL 2) by A15;
LSeg (gk,gk1) = LSeg (g,k) by A3, A4, A11, A17, TOPREAL1:def 3;
then A19: LSeg (g,k) is convex ;
A20: f is_in_general_position_wrt g by A1;
then A21: L~ f misses rng g ;

per cases ) /\ (LSeg (g,k)) = {} or (L~ f) /\ (LSeg (g,k)) = {} ) ;

suppose A22: not (L~ f) /\ (LSeg (g,k)) = {} ; :: thesis:

(L~ f) /\ (LSeg (g,k)) is trivial by A3, A9, A20;
then consider x being object such that
A23: (L~ f) /\ (LSeg (g,k)) = {x} by A22, ZFMISC_1:131;
x in (L~ f) /\ (LSeg (g,k)) by A23, TARSKI:def 1;
then reconsider p = x as Point of (TOP-REAL 2) ;
A24: g /. (k + 1) = g . (k + 1) by A16, PARTFUN1:def 6;
then A25: g /. (k + 1) in rng g by A16, FUNCT_1:3;
A26: g /. k = g . k by A10, PARTFUN1:def 6;
then A27: g /. k in rng g by A10, FUNCT_1:3;

A28: now :: thesis:

assume A29: ( g /. k in L~ f or g /. (k + 1) in L~ f ) ; :: thesis:

per cases by A29;

suppose g /. k in L~ f ; :: thesis:

hence contradiction by A21, A27, XBOOLE_0:3; :: thesis:

end;

suppose g /. (k + 1) in L~ f ; :: thesis:

hence contradiction by A21, A25, XBOOLE_0:3; :: thesis:

end;

rng f misses L~ g by A2;
then A30: rng f misses LSeg ((g /. k),(g /. (k + 1))) by A13, TOPREAL3:19, XBOOLE_1:63;
(L~ f) /\ (LSeg ((g /. k),(g /. (k + 1)))) = {p} by A3, A4, A23, TOPREAL1:def 3;
hence ( card ((L~ f) /\ (LSeg (g,k))) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & g . k in C & g . (k + 1) in C ) ) by A14, A23, A26, A24, A28, A30, Th2, Th32, CARD_1:30; :: thesis:

end;

suppose A31: (L~ f) /\ (LSeg (g,k)) = {} ; :: thesis:

then A32: LSeg (g,k) misses L~ f ;
then A33: ( not g . (k + 1) in RightComp f or not g . k in LeftComp f ) by A19, A12, A18, JORDAN1J:36;

A34: now :: thesis:

per cases by A19, A12, A18, A32, JORDAN1J:36;

suppose A35: not gk in RightComp f ; :: thesis:

A36: LeftComp f is_a_component_of (L~ f) ` by GOBOARD9:def 1;
( gk in LeftComp f & g . (k + 1) in LeftComp f ) by A6, A7, A8, A33, A35, GOBRD14:17;
hence ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & g . k in C & g . (k + 1) in C ) by A36; :: thesis:

end;

suppose A37: not g . (k + 1) in LeftComp f ; :: thesis:

A38: RightComp f is_a_component_of (L~ f) ` by GOBOARD9:def 2;
( g . (k + 1) in RightComp f & g . k in RightComp f ) by A5, A6, A7, A8, A33, A37, GOBRD14:18;
hence ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & g . k in C & g . (k + 1) in C ) by A38; :: thesis:

end;

card ((L~ f) /\ (LSeg (g,k))) = 2 * 0 by A31, CARD_1:27;
hence ( card ((L~ f) /\ (LSeg (g,k))) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & g . k in C & g . (k + 1) in C ) ) by A34; :: thesis:

end;