let f be V8() 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)

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

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

(Cl (RightComp f)) \ (RightComp f) c= Cl (RightComp f)
by XBOOLE_1:36;
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)

end;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 )

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: verumA2: now :: thesis: not x in LeftComp f

assume
not x in RightComp f
; :: thesis: x in L~ fassume
x in LeftComp f
; :: thesis: contradiction

then LeftComp f meets RightComp f by A1, TOPS_1:12;

hence contradiction by Th14; :: thesis: verum

end;then LeftComp f meets RightComp f by A1, TOPS_1:12;

hence contradiction by Th14; :: thesis: verum

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

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