let f be non 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:43;
then A2:
(Rotate f,(N-min (L~ f))) /. 1 = N-min (L~ (Rotate f,(N-min (L~ f))))
by A1, FINSEQ_6:98;
A3:
L~ f = (Cl (RightComp f)) \ (RightComp f)
by Th29;
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
let a be
set ;
:: 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
set 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:115;
A7:
Cl (RightComp f) = (RightComp f) \/ (L~ f)
by Th31;
per cases
( x in RightComp f or x in L~ f )
by A5, A7, XBOOLE_0:def 3;
suppose A8:
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:56, XREAL_1:8;
then
|[(x `1 ),((N-bound (L~ f)) + 1)]| in LeftComp (Rotate f,(N-min (L~ f)))
by A1, A2, JORDAN2C:121;
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 A8, Th37;
then consider c being
set such that A9:
(
c in LSeg x,
|[(x `1 ),((N-bound (L~ f)) + 1)]| &
c in L~ f )
by XBOOLE_0:3;
reconsider c =
c as
Point of
(TOP-REAL 2) by A9;
A10:
|[(x `1 ),((N-bound (L~ f)) + 1)]| `1 = x `1
by EUCLID:56;
proj1 . c =
c `1
by PSCOMP_1:def 28
.=
x `1
by A9, A10, GOBOARD7:5
.=
a
by A6, PSCOMP_1:def 28
;
hence
a in proj1 .: (L~ f)
by A9, FUNCT_2:43;
:: thesis: verum end;
end;
thus
proj1 .: (L~ f) c= proj1 .: (Cl (RightComp f))
by A3, RELAT_1:156, XBOOLE_1:36; :: thesis: verum