let f be constant standard special_circular_sequence; :: thesis: Cl (RightComp f) = (RightComp f) \/ (L~ f)
thus Cl (RightComp f) c= (RightComp f) \/ (L~ f) :: according to XBOOLE_0:def 10 :: thesis: (RightComp f) \/ (L~ f) c= Cl (RightComp f)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Cl (RightComp f) or x in (RightComp f) \/ (L~ f) )
assume A1: x in Cl (RightComp f) ; :: thesis: x in (RightComp f) \/ (L~ f)

now :: thesis: ( not x in RightComp f implies x in L~ f )

A2: now :: thesis: not x in LeftComp f

assume x in LeftComp f ; :: thesis: contradiction
then LeftComp f meets RightComp f by A1, TOPS_1:12;
hence contradiction by Th14; :: thesis: verum

end;

assume not x in RightComp f ; :: thesis: x in L~ f
hence x in L~ f by A1, A2, Th16; :: thesis: verum

end;

hence x in (RightComp f) \/ (L~ f) by XBOOLE_0:def 3; :: thesis: verum

end;

(Cl (RightComp f)) \ (RightComp f) c= Cl (RightComp f) by XBOOLE_1:36;
then ( RightComp f c= Cl (RightComp f) & L~ f c= Cl (RightComp f) ) by Th19, PRE_TOPC:18;
hence (RightComp f) \/ (L~ f) c= Cl (RightComp f) by XBOOLE_1:8; :: thesis: verum