let f, g be FinSequence of (TOP-REAL 2); :: thesis: ( f,g are_in_general_position implies (L~ f) /\ (L~ g) is finite )
assume A1: f,g are_in_general_position ; :: thesis: (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 :: thesis: 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 ; :: thesis: ( 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 ) } ) ; :: thesis: 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; :: thesis: 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; :: thesis: verum