let f be non constant standard special_circular_sequence; 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); ( 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
; 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; ( 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
; ( 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)) = {} )
;
suppose A22:
not
(L~ f) /\ (LSeg (g,k)) = {}
;
( 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 ) )
(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;
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;
verum end;