let f be non constant standard clockwise_oriented special_circular_sequence; :: thesis: for p being Point of (TOP-REAL 2) st p `1 > E-bound (L~ f) holds
p in LeftComp f
let p be Point of (TOP-REAL 2); :: thesis: ( p `1 > E-bound (L~ f) implies p in LeftComp 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;
assume p `1 > E-bound (L~ f) ; :: thesis: p in LeftComp f
then p in LeftComp (Rotate f,(N-min (L~ f))) by A1, A2, JORDAN2C:119;
hence p in LeftComp f by REVROT_1:36; :: thesis: verum