let f be V8() standard special_circular_sequence; :: thesis: Cl (LeftComp f) = (LeftComp f) \/ (L~ f)

thus Cl (LeftComp f) c= (LeftComp f) \/ (L~ f) :: according to XBOOLE_0:def 10 :: thesis: (LeftComp f) \/ (L~ f) c= Cl (LeftComp f)

then ( LeftComp f c= Cl (LeftComp f) & L~ f c= Cl (LeftComp f) ) by Th20, PRE_TOPC:18;

hence (LeftComp f) \/ (L~ f) c= Cl (LeftComp f) by XBOOLE_1:8; :: thesis: verum

thus Cl (LeftComp f) c= (LeftComp f) \/ (L~ f) :: according to XBOOLE_0:def 10 :: thesis: (LeftComp f) \/ (L~ f) c= Cl (LeftComp f)

proof

(Cl (LeftComp f)) \ (LeftComp f) c= Cl (LeftComp f)
by XBOOLE_1:36;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Cl (LeftComp f) or x in (LeftComp f) \/ (L~ f) )

assume A1: x in Cl (LeftComp f) ; :: thesis: x in (LeftComp f) \/ (L~ f)

end;assume A1: x in Cl (LeftComp f) ; :: thesis: x in (LeftComp f) \/ (L~ f)

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

hence
x in (LeftComp f) \/ (L~ f)
by XBOOLE_0:def 3; :: thesis: verumA2:
not x in RightComp f
by A1, Th14, TOPS_1:12;

assume not x in LeftComp f ; :: thesis: x in L~ f

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

end;assume not x in LeftComp f ; :: thesis: x in L~ f

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

then ( LeftComp f c= Cl (LeftComp f) & L~ f c= Cl (LeftComp f) ) by Th20, PRE_TOPC:18;

hence (LeftComp f) \/ (L~ f) c= Cl (LeftComp f) by XBOOLE_1:8; :: thesis: verum