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 Element of 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 Element of 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 Element of 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 k be Element of 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 A2:
( 1 <= k & 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 ) )
A3:
k < len g
by A2, NAT_1:13;
A4:
f is_in_general_position_wrt g
by A1, Def2;
then A5:
L~ f misses rng g
by Def1;
A6:
g is_in_general_position_wrt f
by A1, Def2;
A7:
1 <= k + 1
by A2, NAT_1:13;
A8:
k in dom g
by A2, A3, FINSEQ_3:27;
A9:
k + 1 in dom g
by A2, A7, FINSEQ_3:27;
set m = (L~ f) /\ (LSeg g,k);
A10:
g /. k = g . k
by A8, PARTFUN1:def 8;
A11:
g . k in rng g
by A8, FUNCT_1:12;
A12:
rng g c= the carrier of (TOP-REAL 2)
by FINSEQ_1:def 4;
then reconsider gk = g . k as Point of (TOP-REAL 2) by A11;
g . (k + 1) in rng g
by A9, FUNCT_1:12;
then reconsider gk1 = g . (k + 1) as Point of (TOP-REAL 2) by A12;
A13:
g /. (k + 1) = g . (k + 1)
by A9, PARTFUN1:def 8;
then
LSeg gk,gk1 = LSeg g,k
by A2, A10, TOPREAL1:def 5;
then A14:
LSeg g,k is connected Subset of (TOP-REAL 2)
by GOBOARD9:8;
A15:
g . k in LSeg g,k
by A2, A10, TOPREAL1:27;
A16:
g . (k + 1) in LSeg g,k
by A2, A13, TOPREAL1:27;
A17:
g . k in (L~ f) `
by A1, A2, Th9;
then A18:
not g . k in L~ f
by XBOOLE_0:def 5;
A19:
g . (k + 1) in (L~ f) `
by A1, A2, Th9;
then A20:
not g . (k + 1) in L~ f
by XBOOLE_0:def 5;
set p1 = g /. k;
set p2 = g /. (k + 1);
A21:
LSeg g,k = LSeg (g /. k),(g /. (k + 1))
by A2, TOPREAL1:def 5;
( LSeg g,k is vertical or LSeg g,k is horizontal )
by SPPOL_1:41;
then A22:
( (g /. k) `1 = (g /. (k + 1)) `1 or (g /. k) `2 = (g /. (k + 1)) `2 )
by A21, SPPOL_1:36, SPPOL_1:37;
per cases
( not (L~ f) /\ (LSeg g,k) = {} or (L~ f) /\ (LSeg g,k) = {} )
;
suppose A23:
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 ) )
(L~ f) /\ (LSeg g,k) is
trivial
by A2, A3, A4, Def1;
then consider x being
set such that A24:
(L~ f) /\ (LSeg g,k) = {x}
by A23, REALSET1:def 4;
x in (L~ f) /\ (LSeg g,k)
by A24, TARSKI:def 1;
then reconsider p =
x as
Point of
(TOP-REAL 2) ;
A25:
(
g /. k = g . k &
g /. (k + 1) = g . (k + 1) )
by A8, A9, PARTFUN1:def 8;
A26:
(L~ f) /\ (LSeg (g /. k),(g /. (k + 1))) = {p}
by A2, A24, TOPREAL1:def 5;
A27:
(
g /. k in rng g &
g /. (k + 1) in rng g )
by A8, A9, A25, FUNCT_1:12;
rng f misses L~ g
by A6, Def1;
then
rng f misses LSeg (g /. k),
(g /. (k + 1))
by A21, TOPREAL3:26, XBOOLE_1:63;
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 A22, A24, A25, A26, A28, Th3, Th33, CARD_1:50;
:: thesis: verum end;