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