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)
proof
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)
now :: thesis: ( not x in LeftComp f implies x in L~ f )
A2: 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;
hence x in (LeftComp f) \/ (L~ f) by XBOOLE_0:def 3; :: thesis: verum
end;
(Cl (LeftComp f)) \ (LeftComp f) c= Cl (LeftComp f) by XBOOLE_1:36;
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