let f, g be FinSequence of (TOP-REAL 2); :: thesis: ( f,g are_in_general_position implies for k being Nat holds (L~ f) /\ (LSeg (g,k)) is finite )
assume f,g are_in_general_position ; :: thesis: for k being Nat holds (L~ f) /\ (LSeg (g,k)) is finite
then A1: (L~ f) /\ (L~ g) is finite by Th11;
let k be Nat; :: thesis: (L~ f) /\ (LSeg (g,k)) is finite
((L~ f) /\ (L~ g)) /\ (LSeg (g,k)) = (L~ f) /\ ((L~ g) /\ (LSeg (g,k))) by XBOOLE_1:16
.= (L~ f) /\ (LSeg (g,k)) by TOPREAL3:19, XBOOLE_1:28 ;
hence (L~ f) /\ (LSeg (g,k)) is finite by A1; :: thesis: verum