let f be V22() 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

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