let f be constant standard clockwise_oriented special_circular_sequence; :: thesis: for p being Point of (TOP-REAL 2) st f /. 1 = N-min (L~ f) & p `1 > E-bound (L~ f) holds
p in LeftComp f
let p be Point of (TOP-REAL 2); :: thesis: ( f /. 1 = N-min (L~ f) & p `1 > E-bound (L~ f) implies p in LeftComp f )
assume that
A1: f /. 1 = N-min (L~ f) and
A2: p `1 > E-bound (L~ f) ; :: thesis: p in LeftComp f
set g = SpStSeq (L~ f);
A3: LeftComp (SpStSeq (L~ f)) c= LeftComp f by A1, SPRECT_3:41;
E-bound (L~ (SpStSeq (L~ f))) = E-bound (L~ f) by SPRECT_1:61;
then p in LeftComp (SpStSeq (L~ f)) by A2, SPRECT_3:40;
hence p in LeftComp f by A3; :: thesis: verum