let f be V8() standard clockwise_oriented special_circular_sequence; 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)
XBOOLE_0:def 10 proj2 .: (L~ f) c= proj2 .: (Cl (RightComp f))proof
A3:
Cl (RightComp f) = (RightComp f) \/ (L~ f)
by Th21;
let a be
object ;
TARSKI:def 3 ( not a in proj2 .: (Cl (RightComp f)) or a in proj2 .: (L~ f) )
assume
a in proj2 .: (Cl (RightComp f))
;
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;
suppose A7:
x in RightComp f
;
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;
verum end;
end;
L~ f = (Cl (RightComp f)) \ (RightComp f)
by Th19;
hence
proj2 .: (L~ f) c= proj2 .: (Cl (RightComp f))
by RELAT_1:123, XBOOLE_1:36; verum