let f be non constant standard clockwise_oriented special_circular_sequence; :: thesis: ( f /. 1 = N-min (L~ f) implies LSeg (f /. 1),(f /. 2) c= L~ (SpStSeq (L~ f)) )
assume A1: f /. 1 = N-min (L~ f) ; :: thesis: LSeg (f /. 1),(f /. 2) c= L~ (SpStSeq (L~ f))
then A2: f /. 1 in LSeg (NW-corner (L~ f)),(NE-corner (L~ f)) by Th28;
A3: f /. 2 in N-most (L~ f) by A1, SPRECT_2:34;
N-most (L~ f) c= LSeg (NW-corner (L~ f)),(NE-corner (L~ f)) by XBOOLE_1:17;
then A4: LSeg (f /. 1),(f /. 2) c= LSeg (NW-corner (L~ f)),(NE-corner (L~ f)) by A2, A3, TOPREAL1:12;
LSeg (NW-corner (L~ f)),(NE-corner (L~ f)) c= L~ (SpStSeq (L~ f)) by Th26;
hence LSeg (f /. 1),(f /. 2) c= L~ (SpStSeq (L~ f)) by A4, XBOOLE_1:1; :: thesis: verum