let f1, f2, g1, g2 be FinSequence of (TOP-REAL 2); :: thesis: ( f1 ^' f2,g1 ^' g2 are_in_general_position implies f1 ^' f2,g1 are_in_general_position )
assume A1: f1 ^' f2,g1 ^' g2 are_in_general_position ; :: thesis: f1 ^' f2,g1 are_in_general_position
A2: g1 ^' g2 is_in_general_position_wrt f1 ^' f2 by A1, Def2;

A3: now

let i be Element of NAT ; :: thesis: ( 1 <= i & i < len (f1 ^' f2) implies (L~ g1) /\ (LSeg ((f1 ^' f2),i)) is trivial )
assume ( 1 <= i & i < len (f1 ^' f2) ) ; :: thesis: (L~ g1) /\ (LSeg ((f1 ^' f2),i)) is trivial
then A4: (L~ (g1 ^' g2)) /\ (LSeg ((f1 ^' f2),i)) is trivial by A2, Def1;
(L~ g1) /\ (LSeg ((f1 ^' f2),i)) c= (L~ (g1 ^' g2)) /\ (LSeg ((f1 ^' f2),i)) by Th6, XBOOLE_1:26;
hence (L~ g1) /\ (LSeg ((f1 ^' f2),i)) is trivial by A4; :: thesis: verum

end;

A5: f1 ^' f2 is_in_general_position_wrt g1 ^' g2 by A1, Def2;

A6: now

let i be Element of NAT ; :: thesis: ( 1 <= i & i < len g1 implies (L~ (f1 ^' f2)) /\ (LSeg (g1,i)) is trivial )
assume that
A7: 1 <= i and
A8: i < len g1 ; :: thesis: (L~ (f1 ^' f2)) /\ (LSeg (g1,i)) is trivial
len g1 <= len (g1 ^' g2) by TOPREAL8:7;
then i < len (g1 ^' g2) by A8, XXREAL_0:2;
then (L~ (f1 ^' f2)) /\ (LSeg ((g1 ^' g2),i)) is trivial by A5, A7, Def1;
hence (L~ (f1 ^' f2)) /\ (LSeg (g1,i)) is trivial by A8, TOPREAL8:28; :: thesis: verum

end;

L~ (g1 ^' g2) misses rng (f1 ^' f2) by A2, Def1;
then L~ g1 misses rng (f1 ^' f2) by Th6, XBOOLE_1:63;
then A9: g1 is_in_general_position_wrt f1 ^' f2 by A3, Def1;
L~ (f1 ^' f2) misses rng (g1 ^' g2) by A5, Def1;
then L~ (f1 ^' f2) misses rng g1 by TOPREAL8:10, XBOOLE_1:63;
then f1 ^' f2 is_in_general_position_wrt g1 by A6, Def1;
hence f1 ^' f2,g1 are_in_general_position by A9, Def2; :: thesis: verum