theorem :: GOBRD14:13

for f being non constant standard special_circular_sequence
for A1, A2 being Subset of (TOP-REAL 2) st (L~ f) ` = A1 \/ A2 & A1 misses A2 & ( for C1, C2 being Subset of ((TOP-REAL 2) | ((L~ f) `)) st C1 = A1 & C2 = A2 holds
( C1 is a_component & C2 is a_component ) ) & not ( A1 = RightComp f & A2 = LeftComp f ) holds
( A1 = LeftComp f & A2 = RightComp f )