let f1, f2, g1, g2 be special FinSequence of (TOP-REAL 2); :: thesis:
assume that
A1: f1 ^' f2 is non constant standard special_circular_sequence and
A2: g1 ^' g2 is non constant standard special_circular_sequence and
A3: L~ f1 misses L~ g2 and
A4: L~ f2 misses L~ g1 and
A5: f1 ^' f2,g1 ^' g2 are_in_general_position ; :: thesis:
let p1, p2, q1, q2 be Point of (TOP-REAL 2); :: thesis:
assume that
A6: f1 . 1 = p1 and
A7: f1 . (len f1) = p2 and
A8: g1 . 1 = q1 and
A9: g1 . (len g1) = q2 and
A10: f1 /. (len f1) = f2 /. 1 and
A11: g1 /. (len g1) = g2 /. 1 and
A12: p1 in (L~ f1) /\ (L~ f2) and
A13: q1 in (L~ g1) /\ (L~ g2) and
A14: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (f1 ^' f2)) ` & q1 in C & q2 in C ) ; :: thesis:

A15: now

assume A16: ( len g1 = 0 or len g1 = 1 or len g2 = 0 or len g2 = 1 ) ; :: thesis:

per cases by A16;

suppose ( len g1 = 0 or len g1 = 1 ) ; :: thesis:

then L~ g1 = {} by TOPREAL1:28;
hence contradiction by A13; :: thesis:

end;

suppose ( len g2 = 0 or len g2 = 1 ) ; :: thesis:

then L~ g2 = {} by TOPREAL1:28;
hence contradiction by A13; :: thesis:

end;

then A17: not len g1 is trivial by NAT_2:def 1;
then A18: len g1 >= 2 by NAT_2:31;
A19: not g1 is empty by A17, Lm3;
A20: not len g2 is trivial by A15, NAT_2:def 1;
then A21: len g2 >= 1 + 1 by NAT_2:31;
A22: not g2 is trivial by A20, Lm3;

A23: now

assume A24: ( len f1 = 0 or len f1 = 1 or len f2 = 0 or len f2 = 1 ) ; :: thesis:

per cases by A24;

suppose ( len f1 = 0 or len f1 = 1 ) ; :: thesis:

then L~ f1 = {} by TOPREAL1:28;
hence contradiction by A12; :: thesis:

end;

suppose ( len f2 = 0 or len f2 = 1 ) ; :: thesis:

then L~ f2 = {} by TOPREAL1:28;
hence contradiction by A12; :: thesis:

end;

then A25: not len f1 is trivial by NAT_2:def 1;
then A26: len f1 >= 2 by NAT_2:31;
A27: not f1 is empty by A25, Lm3;
A28: not len f2 is trivial by A23, NAT_2:def 1;
then A29: len f2 >= 1 + 1 by NAT_2:31;
not f2 is trivial by A28, Lm3;
then A30: (L~ (f1 ^' f2)) /\ (L~ g1) = ((L~ f1) \/ (L~ f2)) /\ (L~ g1) by A10, A27, TOPREAL8:35
.= ((L~ f1) /\ (L~ g1)) \/ ((L~ f2) /\ (L~ g1)) by XBOOLE_1:23
.= ((L~ f1) /\ (L~ g1)) \/ {} by A4, XBOOLE_0:def 7
.= ((L~ f1) /\ (L~ g1)) \/ ((L~ f1) /\ (L~ g2)) by A3, XBOOLE_0:def 7
.= ((L~ g1) \/ (L~ g2)) /\ (L~ f1) by XBOOLE_1:23
.= (L~ f1) /\ (L~ (g1 ^' g2)) by A11, A19, A22, TOPREAL8:35 ;
A31: ( f1 ^' f2,g1 are_in_general_position & g1 is unfolded & g1 is s.n.c. ) by A2, A5, A21, Th5, Th8;
A32: ( g1 ^' g2,f1 are_in_general_position & f1 is unfolded & f1 is s.n.c. ) by A1, A5, A29, Th5, Th8;
card ((L~ (f1 ^' f2)) /\ (L~ g1)) is even Element of NAT by A1, A8, A9, A14, A18, A31, Th35;
hence ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (g1 ^' g2)) ` & p1 in C & p2 in C ) by A2, A6, A7, A26, A30, A32, Th35; :: thesis: