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