let f, g be FinSequence of (TOP-REAL 2); ( 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
; 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; (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; verum