let f be non constant 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: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
proj2 .: (Cl (RightComp f)) c= proj2 .: (L~ f)
:: according to XBOOLE_0:def 10 :: thesis: proj2 .: (L~ f) c= proj2 .: (Cl (RightComp f))proof
let a be
set ;
:: 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
set 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: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 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:56, XREAL_1:8;
then
|[((E-bound (L~ f)) + 1),(x `2 )]| in LeftComp (Rotate f,(N-min (L~ f)))
by A1, A2, JORDAN2C:119;
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 A8, Th37;
then consider c being
set such that A9:
(
c in LSeg x,
|[((E-bound (L~ f)) + 1),(x `2 )]| &
c in L~ f )
by XBOOLE_0:3;
reconsider c =
c as
Point of
(TOP-REAL 2) by A9;
A10:
|[((E-bound (L~ f)) + 1),(x `2 )]| `2 = x `2
by EUCLID:56;
proj2 . c =
c `2
by PSCOMP_1:def 29
.=
x `2
by A9, A10, GOBOARD7:6
.=
a
by A6, PSCOMP_1:def 29
;
hence
a in proj2 .: (L~ f)
by A9, FUNCT_2:43;
:: thesis: verum end;
end;
thus
proj2 .: (L~ f) c= proj2 .: (Cl (RightComp f))
by A3, RELAT_1:156, XBOOLE_1:36; :: thesis: verum