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:24;
(Cl (LeftComp f)) \/ (RightComp f) = ((L~ f) \/ (LeftComp f)) \/ (RightComp f) by GOBRD14:22
.= ((L~ f) \/ (RightComp f)) \/ (LeftComp f) by XBOOLE_1:4
.= the carrier of (TOP-REAL 2) by GOBRD14:15 ;
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:14;
( Cl (LeftComp f) = (LeftComp f) \/ (L~ f) & L~ f misses RightComp f ) by GOBRD14:22, SPRECT_3:25;
then Cl (LeftComp f) misses RightComp f by A2, XBOOLE_1:70;
hence RightComp f c= (Cl (LeftComp f)) ` by SUBSET_1:23; :: thesis: verum