let f be non constant standard special_circular_sequence; :: thesis: for g being special FinSequence of () st f,g are_in_general_position holds
for k being Nat st 1 <= k & k + 1 <= len g holds
( card ((L~ f) /\ (LSeg (g,k))) is even Element of NAT iff ex C being Subset of () st
( C is_a_component_of (L~ f) ` & g . k in C & g . (k + 1) in C ) )

let g be special FinSequence of (); :: thesis: ( f,g are_in_general_position implies for k being Nat st 1 <= k & k + 1 <= len g holds
( card ((L~ f) /\ (LSeg (g,k))) is even Element of NAT iff ex C being Subset of () st
( C is_a_component_of (L~ f) ` & g . k in C & g . (k + 1) in C ) ) )

assume A1: f,g are_in_general_position ; :: thesis: for k being Nat st 1 <= k & k + 1 <= len g holds
( card ((L~ f) /\ (LSeg (g,k))) is even Element of NAT iff ex C being Subset of () st
( C is_a_component_of (L~ f) ` & g . k in C & g . (k + 1) in C ) )

A2: g is_in_general_position_wrt f by A1;
let k be Nat; :: thesis: ( 1 <= k & k + 1 <= len g implies ( card ((L~ f) /\ (LSeg (g,k))) is even Element of NAT iff ex C being Subset of () st
( C is_a_component_of (L~ f) ` & g . k in C & g . (k + 1) in C ) ) )

assume that
A3: 1 <= k and
A4: k + 1 <= len g ; :: thesis: ( card ((L~ f) /\ (LSeg (g,k))) is even Element of NAT iff ex C being Subset of () st
( C is_a_component_of (L~ f) ` & g . k in C & g . (k + 1) in C ) )

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 ;
then A10: k in dom g by ;
then A11: g /. k = g . k by PARTFUN1:def 6;
then A12: g . k in LSeg (g,k) by ;
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 ;
( 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 ;
A15: rng g c= the carrier of () by FINSEQ_1:def 4;
1 <= k + 1 by ;
then A16: k + 1 in dom g by ;
then A17: g /. (k + 1) = g . (k + 1) by PARTFUN1:def 6;
then A18: g . (k + 1) in LSeg (g,k) by ;
g . (k + 1) in rng g by ;
then reconsider gk1 = g . (k + 1) as Point of () by A15;
g . k in rng g by ;
then reconsider gk = g . k as Point of () by A15;
LSeg (gk,gk1) = LSeg (g,k) by ;
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: ( card ((L~ f) /\ (LSeg (g,k))) is even Element of NAT iff ex C being Subset of () st
( C is_a_component_of (L~ f) ` & g . k in C & g . (k + 1) in C ) )

(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 ;
x in (L~ f) /\ (LSeg (g,k)) by ;
then reconsider p = x as Point of () ;
A24: g /. (k + 1) = g . (k + 1) by ;
then A25: g /. (k + 1) in rng g by ;
A26: g /. k = g . k by ;
then A27: g /. k in rng g by ;
A28: now :: thesis: ( not g /. k in L~ f & not g /. (k + 1) in L~ f )
assume A29: ( g /. k in L~ f or g /. (k + 1) in L~ f ) ; :: thesis: contradiction
per cases ( g /. k in L~ f or g /. (k + 1) in L~ f ) by A29;
end;
end;
rng f misses L~ g by A2;
then A30: rng f misses LSeg ((g /. k),(g /. (k + 1))) by ;
(L~ f) /\ (LSeg ((g /. k),(g /. (k + 1)))) = {p} by ;
hence ( card ((L~ f) /\ (LSeg (g,k))) is even Element of NAT iff ex C being Subset of () st
( C is_a_component_of (L~ f) ` & g . k in C & g . (k + 1) in C ) ) by ; :: thesis: verum
end;
suppose A31: (L~ f) /\ (LSeg (g,k)) = {} ; :: thesis: ( card ((L~ f) /\ (LSeg (g,k))) is even Element of NAT iff ex C being Subset of () st
( C is_a_component_of (L~ f) ` & g . k in C & g . (k + 1) in C ) )

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 ;
A34: now :: thesis: ex C being Subset of () st
( C is_a_component_of (L~ f) ` & g . k in C & g . (k + 1) in C )
per cases ( not gk in RightComp f or not g . (k + 1) in LeftComp f ) by ;
suppose A35: not gk in RightComp f ; :: thesis: ex C being Subset of () st
( C is_a_component_of (L~ f) ` & g . k in C & g . (k + 1) in C )

A36: LeftComp f is_a_component_of (L~ f) ` by GOBOARD9:def 1;
( gk in LeftComp f & g . (k + 1) in LeftComp f ) by ;
hence ex C being Subset of () st
( C is_a_component_of (L~ f) ` & g . k in C & g . (k + 1) in C ) by A36; :: thesis: verum
end;
suppose A37: not g . (k + 1) in LeftComp f ; :: thesis: ex C being Subset of () st
( C is_a_component_of (L~ f) ` & g . k in C & g . (k + 1) in C )

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 () st
( C is_a_component_of (L~ f) ` & g . k in C & g . (k + 1) in C ) by A38; :: thesis: verum
end;
end;
end;
card ((L~ f) /\ (LSeg (g,k))) = 2 * 0 by ;
hence ( card ((L~ f) /\ (LSeg (g,k))) is even Element of NAT iff ex C being Subset of () st
( C is_a_component_of (L~ f) ` & g . k in C & g . (k + 1) in C ) ) by A34; :: thesis: verum
end;
end;