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