for f1, f2, g1 being special FinSequence of (TOP-REAL 2) st f1 ^' f2 is non constant standard special_circular_sequence & f1 ^' f2,g1 are_in_general_position & len g1 >= 2 & g1 is unfolded & g1 is s.n.c. holds
( card ((L~ (f1 ^' f2)) /\ (L~ g1)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (f1 ^' f2)) ` & g1 . 1 in C & g1 . (len g1) in C ) )