theorem Th30: :: GOBRD14:30

for f being constant standard clockwise_oriented special_circular_sequence holds proj2 .: (Cl (RightComp f)) = proj2 .: (L~ f)