let f be non constant standard clockwise_oriented special_circular_sequence; :: thesis: proj2 .: (Cl (RightComp f)) = proj2 .: (L~ f)
set g = Rotate (f,(N-min (L~ f)));
A1: L~ f = L~ (Rotate (f,(N-min (L~ f)))) by REVROT_1:33;
N-min (L~ f) in rng f by SPRECT_2:43;
then A2: (Rotate (f,(N-min (L~ f)))) /. 1 = N-min (L~ (Rotate (f,(N-min (L~ f))))) by A1, FINSEQ_6:98;
thus proj2 .: (Cl (RightComp f)) c= proj2 .: (L~ f) :: according to XBOOLE_0:def 10 :: thesis: proj2 .: (L~ f) c= proj2 .: (Cl (RightComp f))

proof

A3: Cl (RightComp f) = (RightComp f) \/ (L~ f) by Th31;
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in proj2 .: (Cl (RightComp f)) or a in proj2 .: (L~ f) )
assume a in proj2 .: (Cl (RightComp f)) ; :: thesis: a in proj2 .: (L~ f)
then consider x being set such that
A4: x in the carrier of (TOP-REAL 2) and
A5: x in Cl (RightComp f) and
A6: a = proj2 . x by FUNCT_2:115;

per cases ( x in RightComp f or x in L~ f ) by A5, A3, XBOOLE_0:def 3;

suppose A7: x in RightComp f ; :: thesis: a in proj2 .: (L~ f)

reconsider x = x as Point of (TOP-REAL 2) by A4;
set b = |[((E-bound (L~ f)) + 1),(x `2)]|;
( |[((E-bound (L~ f)) + 1),(x `2)]| `1 = (E-bound (L~ f)) + 1 & (E-bound (L~ f)) + 1 > (E-bound (L~ f)) + 0 ) by EUCLID:56, XREAL_1:8;
then |[((E-bound (L~ f)) + 1),(x `2)]| in LeftComp (Rotate (f,(N-min (L~ f)))) by A1, A2, JORDAN2C:119;
then |[((E-bound (L~ f)) + 1),(x `2)]| in LeftComp f by REVROT_1:36;
then LSeg (x,|[((E-bound (L~ f)) + 1),(x `2)]|) meets L~ f by A7, Th37;
then consider c being set such that
A8: c in LSeg (x,|[((E-bound (L~ f)) + 1),(x `2)]|) and
A9: c in L~ f by XBOOLE_0:3;
reconsider c = c as Point of (TOP-REAL 2) by A8;
A10: |[((E-bound (L~ f)) + 1),(x `2)]| `2 = x `2 by EUCLID:56;
proj2 . c = c `2 by PSCOMP_1:def 29
.= x `2 by A8, A10, GOBOARD7:6
.= a by A6, PSCOMP_1:def 29 ;
hence a in proj2 .: (L~ f) by A9, FUNCT_2:43; :: thesis: verum

end;

suppose x in L~ f ; :: thesis: a in proj2 .: (L~ f)

hence a in proj2 .: (L~ f) by A6, FUNCT_2:43; :: thesis: verum

end;

end;

end;

L~ f = (Cl (RightComp f)) \ (RightComp f) by Th29;
hence proj2 .: (L~ f) c= proj2 .: (Cl (RightComp f)) by RELAT_1:156, XBOOLE_1:36; :: thesis: verum