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