let f be 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:30;
A4: LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) c= L~ (SpStSeq (L~ f)) by Th14;
f /. 1 in LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by A2, Th15;
then LSeg ((f /. 1),(f /. 2)) c= LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by A3, A1, TOPREAL1:6;
hence LSeg ((f /. 1),(f /. 2)) c= L~ (SpStSeq (L~ f)) by A4; :: thesis: verum