let f be non constant standard special_circular_sequence; :: thesis: (Cl (RightComp f)) ` = LeftComp f
A1: (Cl (RightComp f)) ` misses Cl (RightComp f) by SUBSET_1:24;
(Cl (RightComp f)) \/ (LeftComp f) = ((L~ f) \/ (RightComp f)) \/ (LeftComp f) by GOBRD14:21
.= the carrier of (TOP-REAL 2) by GOBRD14:15 ;
hence (Cl (RightComp f)) ` c= LeftComp f by A1, XBOOLE_1:73; :: according to XBOOLE_0:def 10 :: thesis: LeftComp f c= (Cl (RightComp f)) `
A2: LeftComp f misses RightComp f by GOBRD14:14;
( Cl (RightComp f) = (RightComp f) \/ (L~ f) & L~ f misses LeftComp f ) by GOBRD14:21, SPRECT_3:26;
then Cl (RightComp f) misses LeftComp f by A2, XBOOLE_1:70;
hence LeftComp f c= (Cl (RightComp f)) ` by SUBSET_1:23; :: thesis: verum