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;
A3: now :: thesis: for i being Nat st 1 <= i & i < len (f1 ^' f2) holds
(L~ g1) /\ (LSeg ((f1 ^' f2),i)) is trivial
let i be 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;
(L~ g1) /\ (LSeg ((f1 ^' f2),i)) c= (L~ (g1 ^' g2)) /\ (LSeg ((f1 ^' f2),i)) by Th5, 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;
A6: now :: thesis: for i being Nat st 1 <= i & i < len g1 holds
(L~ (f1 ^' f2)) /\ (LSeg (g1,i)) is trivial
let i be 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;
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;
then L~ g1 misses rng (f1 ^' f2) by Th5, XBOOLE_1:63;
then A9: g1 is_in_general_position_wrt f1 ^' f2 by A3;
L~ (f1 ^' f2) misses rng (g1 ^' g2) by A5;
then L~ (f1 ^' f2) misses rng g1 by TOPREAL8:10, XBOOLE_1:63;
then f1 ^' f2 is_in_general_position_wrt g1 by A6;
hence f1 ^' f2,g1 are_in_general_position by A9; :: thesis: verum