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