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 AL = { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ;
set BL = { (LSeg g,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len g ) } ;
A2: (L~ f) /\ (L~ g) = union (INTERSECTION { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ,{ (LSeg g,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len g ) } ) by SETFAM_1:39;
A3: INTERSECTION { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ,{ (LSeg g,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len g ) } is finite by Th11;

now

let Z be set ; :: thesis: ( Z in INTERSECTION { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ,{ (LSeg g,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len g ) } implies Z is finite )
assume A4: Z in INTERSECTION { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ,{ (LSeg g,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len g ) } ; :: thesis: Z is finite
consider X, Y being set such that
A5: ( X in { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } & Y in { (LSeg g,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len g ) } & Z = X /\ Y ) by A4, SETFAM_1:def 5;
consider i being Element of NAT such that
A6: ( X = LSeg f,i & 1 <= i & i + 1 <= len f ) by A5;
consider j being Element of NAT such that
A7: ( Y = LSeg g,j & 1 <= j & j + 1 <= len g ) by A5;
Z is trivial set by A1, A5, A6, A7, Th10;
hence Z is finite ; :: thesis: verum

end;

hence (L~ f) /\ (L~ g) is finite by A2, A3, FINSET_1:25; :: thesis: verum