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

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