let f be V8() 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: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 proj2 .: (Cl (RightComp f)) c= proj2 .: (L~ f) :: according to XBOOLE_0:def 10 :: thesis: proj2 .: (L~ f) c= proj2 .: (Cl (RightComp f))

hence proj2 .: (L~ f) c= proj2 .: (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 proj2 .: (Cl (RightComp f)) c= proj2 .: (L~ f) :: according to XBOOLE_0:def 10 :: thesis: proj2 .: (L~ f) c= proj2 .: (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 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 object 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:64;

end;let a be object ; :: 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 object 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: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 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:52, XREAL_1:6;

then |[((E-bound (L~ f)) + 1),(x `2)]| in LeftComp (Rotate (f,(N-min (L~ f)))) by A1, A2, JORDAN2C:111;

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, Th27;

then consider c being object 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:52;

proj2 . c = c `2 by PSCOMP_1:def 6

.= x `2 by A8, A10, GOBOARD7:6

.= a by A6, PSCOMP_1:def 6 ;

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

end;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:52, XREAL_1:6;

then |[((E-bound (L~ f)) + 1),(x `2)]| in LeftComp (Rotate (f,(N-min (L~ f)))) by A1, A2, JORDAN2C:111;

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, Th27;

then consider c being object 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:52;

proj2 . c = c `2 by PSCOMP_1:def 6

.= x `2 by A8, A10, GOBOARD7:6

.= a by A6, PSCOMP_1:def 6 ;

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

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