let f be V8() standard special_circular_sequence; :: thesis: ((L~ f) \/ (RightComp f)) \/ (LeftComp f) = the carrier of (TOP-REAL 2)
A1: ((L~ f) `) \/ (L~ f) = [#] the carrier of (TOP-REAL 2) by SUBSET_1:10
.= the carrier of (TOP-REAL 2) ;
(L~ f) ` = (RightComp f) \/ (LeftComp f) by GOBRD12:10;
hence ((L~ f) \/ (RightComp f)) \/ (LeftComp f) = the carrier of (TOP-REAL 2) by A1, XBOOLE_1:4; :: thesis: verum