let f be non constant standard special_circular_sequence; :: thesis: for g being special FinSequence of (TOP-REAL 2) 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 (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & g . k in C & g . (k + 1) in C ) )

let g be special FinSequence of (TOP-REAL 2); :: 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 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 ;

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 (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & g . k in C & g . (k + 1) in C ) )

let g be special FinSequence of (TOP-REAL 2); :: 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 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
( not (L~ f) /\ (LSeg (g,k)) = {} or (L~ f) /\ (LSeg (g,k)) = {} )
;

end;

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 (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & g . k in C & g . (k + 1) in C ) )

( 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 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;

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: verum

end;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: ( not g /. k in L~ f & not g /. (k + 1) in L~ f )

rng f misses L~ g
by A2;assume A29:
( g /. k in L~ f or g /. (k + 1) in L~ f )
; :: thesis: contradiction

end;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: verum

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 (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & g . k in C & g . (k + 1) in C ) )

( 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 A19, A12, A18, JORDAN1J:36;

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: verum

end;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: 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 )end;

card ((L~ f) /\ (LSeg (g,k))) = 2 * 0
by A31, CARD_1:27;( 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 A19, A12, A18, A32, JORDAN1J:36;

end;

suppose A35:
not gk in RightComp f
; :: thesis: 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 )

( 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 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: verum

end;( 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: verum

suppose A37:
not g . (k + 1) in LeftComp f
; :: thesis: 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 )

( 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 (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & g . k in C & g . (k + 1) in C ) by A38; :: thesis: verum

end;( 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: verum

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: verum