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)) )
A1: N-most (L~ f) c= LSeg (NW-corner (L~ f)),(NE-corner (L~ f)) by XBOOLE_1:17;
assume A2: f /. 1 = N-min (L~ f) ; :: thesis: LSeg (f /. 1),(f /. 2) c= L~ (SpStSeq (L~ f))
then A3: f /. 2 in N-most (L~ f) by SPRECT_2:34;
A4: LSeg (NW-corner (L~ f)),(NE-corner (L~ f)) c= L~ (SpStSeq (L~ f)) by Th26;
f /. 1 in LSeg (NW-corner (L~ f)),(NE-corner (L~ f)) by A2, Th28;
then LSeg (f /. 1),(f /. 2) c= LSeg (NW-corner (L~ f)),(NE-corner (L~ f)) by A3, A1, TOPREAL1:12;
hence LSeg (f /. 1),(f /. 2) c= L~ (SpStSeq (L~ f)) by A4, XBOOLE_1:1; :: thesis: verum