theorem Th21: :: GOBRD14:21

for f being non constant standard special_circular_sequence holds Cl (RightComp f) = (RightComp f) \/ (L~ f)