let f be constant standard special_circular_sequence; :: thesis: LeftComp f misses L~ f
(L~ f) ` = (LeftComp f) \/ (RightComp f) by GOBRD12:10;
then LeftComp f c= (L~ f) ` by XBOOLE_1:7;
hence LeftComp f misses L~ f by SUBSET_1:23; :: thesis: verum