let f be V22() standard clockwise_oriented special_circular_sequence; :: thesis: for p being Point of (TOP-REAL 2) st p `1 < W-bound (L~ f) holds

p in LeftComp f

let p be Point of (TOP-REAL 2); :: thesis: ( p `1 < W-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 `1 < W-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:110;

hence p in LeftComp f by REVROT_1:36; :: thesis: verum

p in LeftComp f

let p be Point of (TOP-REAL 2); :: thesis: ( p `1 < W-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 `1 < W-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:110;

hence p in LeftComp f by REVROT_1:36; :: thesis: verum