let f be constant standard clockwise_oriented special_circular_sequence; :: thesis: for p being Point of (TOP-REAL 2) st p `2 > N-bound (L~ f) holds
p in LeftComp f
let p be Point of (TOP-REAL 2); :: thesis: ( p `2 > N-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;
assume A2: p `2 > N-bound (L~ f) ; :: thesis: p in LeftComp f
N-min (L~ f) in rng f by SPRECT_2:39;
then (Rotate (f,(N-min (L~ f)))) /. 1 = N-min (L~ (Rotate (f,(N-min (L~ f))))) by A1, FINSEQ_6:92;
then p in LeftComp (Rotate (f,(N-min (L~ f)))) by A1, A2, JORDAN2C:113;
hence p in LeftComp f by REVROT_1:36; :: thesis: verum