let f1, f2, g1, g2 be FinSequence of (TOP-REAL 2); ( 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
; f1 ^' f2,g1 are_in_general_position
A2:
g1 ^' g2 is_in_general_position_wrt f1 ^' f2
by A1;
A5:
f1 ^' f2 is_in_general_position_wrt g1 ^' g2
by A1;
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; verum