:: deftheorem Def2 defines RightComp GOBOARD9:def 2 :
for f being non constant standard special_circular_sequence
for b₂ being Subset of (TOP-REAL 2) holds
( b₂ = RightComp f iff ( b₂ is_a_component_of (L~ f) ` & Int (right_cell (f,1)) c= b₂ ) );