begin
begin
begin
begin
begin
begin
begin
Lm1:
for f being non constant standard special_circular_sequence
for i, j being Element of NAT st i in dom f & j in dom f & mid (f,i,j) is S-Sequence_in_R2 & f /. i = N-min (L~ f) & N-min (L~ f) <> NW-corner (L~ f) & f /. j = N-max (L~ f) & N-max (L~ f) <> NE-corner (L~ f) holds
(<*(NW-corner (L~ f))*> ^ (mid (f,i,j))) ^ <*(NE-corner (L~ f))*> is S-Sequence_in_R2
Lm2:
for f being non constant standard special_circular_sequence holds LSeg ((S-max (L~ f)),(SE-corner (L~ f))) misses LSeg ((NW-corner (L~ f)),(N-min (L~ f)))
Lm3:
for f being non constant standard special_circular_sequence
for i, j being Element of NAT st i in dom f & j in dom f & mid (f,i,j) is S-Sequence_in_R2 & f /. i = N-min (L~ f) & N-min (L~ f) <> NW-corner (L~ f) & f /. j = S-max (L~ f) & S-max (L~ f) <> SE-corner (L~ f) holds
(<*(NW-corner (L~ f))*> ^ (mid (f,i,j))) ^ <*(SE-corner (L~ f))*> is S-Sequence_in_R2
begin
Lm4:
for f being non constant standard special_circular_sequence st f /. 1 = N-min (L~ f) holds
(N-min (L~ f)) .. f < (E-max (L~ f)) .. f
Lm5:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) holds
(N-max (L~ z)) .. z < (S-max (L~ z)) .. z
Lm6:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) holds
(N-max (L~ z)) .. z < (S-min (L~ z)) .. z
Lm7:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) holds
(E-max (L~ z)) .. z < (S-max (L~ z)) .. z
Lm8:
for f being non constant standard special_circular_sequence holds (LSeg ((N-min (L~ f)),(NW-corner (L~ f)))) /\ (LSeg ((NE-corner (L~ f)),(E-max (L~ f)))) = {}
Lm9:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) holds
(E-min (L~ z)) .. z < (S-min (L~ z)) .. z
Lm10:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) & N-min (L~ z) <> W-max (L~ z) holds
(E-min (L~ z)) .. z < (W-max (L~ z)) .. z
Lm11:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) holds
(E-min (L~ z)) .. z < (W-min (L~ z)) .. z