let f, g be FinSequence of (TOP-REAL 2); ( f,g are_in_general_position implies (L~ f) /\ (L~ g) is finite )
assume A1:
f,g are_in_general_position
; (L~ f) /\ (L~ g) is finite
set BL = { (LSeg (g,j)) where j is Nat : ( 1 <= j & j + 1 <= len g ) } ;
set AL = { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } ;
A2:
now for Z being set st Z in INTERSECTION ( { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } , { (LSeg (g,j)) where j is Nat : ( 1 <= j & j + 1 <= len g ) } ) holds
Z is finite let Z be
set ;
( Z in INTERSECTION ( { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } , { (LSeg (g,j)) where j is Nat : ( 1 <= j & j + 1 <= len g ) } ) implies Z is finite )assume
Z in INTERSECTION (
{ (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } ,
{ (LSeg (g,j)) where j is Nat : ( 1 <= j & j + 1 <= len g ) } )
;
Z is finite then consider X,
Y being
set such that A3:
(
X in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } &
Y in { (LSeg (g,j)) where j is Nat : ( 1 <= j & j + 1 <= len g ) } )
and A4:
Z = X /\ Y
by SETFAM_1:def 5;
( ex
i being
Nat st
(
X = LSeg (
f,
i) & 1
<= i &
i + 1
<= len f ) & ex
j being
Nat st
(
Y = LSeg (
g,
j) & 1
<= j &
j + 1
<= len g ) )
by A3;
hence
Z is
finite
by A1, A4, Th9;
verum end;
( (L~ f) /\ (L~ g) = union (INTERSECTION ( { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } , { (LSeg (g,j)) where j is Nat : ( 1 <= j & j + 1 <= len g ) } )) & INTERSECTION ( { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } , { (LSeg (g,j)) where j is Nat : ( 1 <= j & j + 1 <= len g ) } ) is finite )
by Th10, SETFAM_1:28;
hence
(L~ f) /\ (L~ g) is finite
by A2, FINSET_1:7; verum