let f be V8() standard clockwise_oriented special_circular_sequence; :: thesis: proj1 .: (Cl ()) = 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 ;
thus proj1 .: (Cl ()) c= proj1 .: (L~ f) :: according to XBOOLE_0:def 10 :: thesis: proj1 .: (L~ f) c= proj1 .: (Cl ())
proof
A3: Cl () = () \/ (L~ f) by Th21;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in proj1 .: (Cl ()) or a in proj1 .: (L~ f) )
assume a in proj1 .: (Cl ()) ; :: thesis: a in proj1 .: (L~ f)
then consider x being object such that
A4: x in the carrier of () and
A5: x in Cl () and
A6: a = proj1 . x by FUNCT_2:64;
per cases ( x in RightComp f or x in L~ f ) by ;
suppose A7: x in RightComp f ; :: thesis: a in proj1 .: (L~ f)
reconsider x = x as Point of () 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 ;
then |[(x `1),((N-bound (L~ f)) + 1)]| in LeftComp (Rotate (f,(N-min (L~ f)))) by ;
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 ;
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 () 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
.= a by ;
hence a in proj1 .: (L~ f) by ; :: thesis: verum
end;
end;
end;
L~ f = (Cl ()) \ () by Th19;
hence proj1 .: (L~ f) c= proj1 .: (Cl ()) by ; :: thesis: verum