theorem Th19: :: GOBRD14:19

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