let f be non constant standard clockwise_oriented special_circular_sequence; :: thesis: for p being Point of (TOP-REAL 2) st f /. 1 = N-min (L~ f) & p `2 < S-bound (L~ f) holds
p in LeftComp f
let p be Point of (TOP-REAL 2); :: thesis: ( f /. 1 = N-min (L~ f) & p `2 < S-bound (L~ f) implies p in LeftComp f )
assume A1: ( f /. 1 = N-min (L~ f) & p `2 < S-bound (L~ f) ) ; :: thesis: p in LeftComp f
set g = SpStSeq (L~ f);
S-bound (L~ (SpStSeq (L~ f))) = S-bound (L~ f) by SPRECT_1:67;
then A2: p in LeftComp (SpStSeq (L~ f)) by A1, SPRECT_3:57;
LeftComp (SpStSeq (L~ f)) c= LeftComp f by A1, SPRECT_3:58;
hence p in LeftComp f by A2; :: thesis: verum