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

hence proj1 .: (L~ f) c= proj1 .: (Cl (RightComp f)) by RELAT_1:123, XBOOLE_1:36; :: thesis: verum

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

L~ f = (Cl (RightComp f)) \ (RightComp f)
by Th19;
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;

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

end;

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 EUCLID:52, 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 by EUCLID:52;

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;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 EUCLID:52, 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 by EUCLID:52;

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

hence proj1 .: (L~ f) c= proj1 .: (Cl (RightComp f)) by RELAT_1:123, XBOOLE_1:36; :: thesis: verum