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

(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