let f be constant standard clockwise_oriented special_circular_sequence; :: thesis: proj1 .: (Cl (RightComp f)) = proj1 .: (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:39;
then A2: (Rotate (f,(N-min (L~ f)))) /. 1 = N-min (L~ (Rotate (f,(N-min (L~ f))))) by A1, FINSEQ_6:92;
thus proj1 .: (Cl (RightComp f)) c= proj1 .: (L~ f) :: according to XBOOLE_0:def 10 :: thesis: proj1 .: (L~ f) c= proj1 .: (Cl (RightComp f))
proof
A3: Cl (RightComp f) = (RightComp f) \/ (L~ f) by Th21;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in proj1 .: (Cl (RightComp f)) or a in proj1 .: (L~ f) )
assume a in proj1 .: (Cl (RightComp f)) ; :: thesis: a in proj1 .: (L~ f)
then consider x being object such that
A4: x in the carrier of (TOP-REAL 2) and
A5: x in Cl (RightComp f) and
A6: a = proj1 . x by FUNCT_2:64;
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 proj1 .: (L~ f)
reconsider x = x as Point of (TOP-REAL 2) by A4;
set b = |[(x `1),((N-bound (L~ f)) + 1)]|;
( |[(x `1),((N-bound (L~ f)) + 1)]| `2 = (N-bound (L~ f)) + 1 & (N-bound (L~ f)) + 1 > (N-bound (L~ f)) + 0 ) by XREAL_1:6;
then |[(x `1),((N-bound (L~ f)) + 1)]| in LeftComp (Rotate (f,(N-min (L~ f)))) by A1, A2, JORDAN2C:113;
then |[(x `1),((N-bound (L~ f)) + 1)]| in LeftComp f by REVROT_1:36;
then LSeg (x,|[(x `1),((N-bound (L~ f)) + 1)]|) meets L~ f by A7, Th27;
then consider c being object such that
A8: c in LSeg (x,|[(x `1),((N-bound (L~ f)) + 1)]|) and
A9: c in L~ f by XBOOLE_0:3;
reconsider c = c as Point of (TOP-REAL 2) by A8;
A10: |[(x `1),((N-bound (L~ f)) + 1)]| `1 = x `1 ;
proj1 . c = c `1 by PSCOMP_1:def 5
.= x `1 by A8, A10, GOBOARD7:5
.= a by A6, PSCOMP_1:def 5 ;
hence a in proj1 .: (L~ f) by A9, FUNCT_2:35; :: thesis: verum
end;
end;
end;
L~ f = (Cl (RightComp f)) \ (RightComp f) by Th19;
hence proj1 .: (L~ f) c= proj1 .: (Cl (RightComp f)) by RELAT_1:123, XBOOLE_1:36; :: thesis: verum