:: Again on the Order on a Special Polygon
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received October 16, 2000
:: Copyright (c) 2000 Association of Mizar Users
theorem Th1: :: SPRECT_5:1
theorem Th2: :: SPRECT_5:2
theorem Th3: :: SPRECT_5:3
theorem Th4: :: SPRECT_5:4
theorem Th5: :: SPRECT_5:5
theorem :: SPRECT_5:6
theorem Th7: :: SPRECT_5:7
theorem Th8: :: SPRECT_5:8
theorem Th9: :: SPRECT_5:9
theorem Th10: :: SPRECT_5:10
theorem Th11: :: SPRECT_5:11
theorem Th12: :: SPRECT_5:12
theorem :: SPRECT_5:13
theorem :: SPRECT_5:14
theorem :: SPRECT_5:15
theorem :: SPRECT_5:16
theorem :: SPRECT_5:17
theorem :: SPRECT_5:18
theorem :: SPRECT_5:19
theorem :: SPRECT_5:20
theorem :: SPRECT_5:21
Lm1:
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
Lm2:
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-min (L~ z)) .. z
Lm3:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) holds
(E-max (L~ z)) .. z < (W-min (L~ z)) .. z
Lm4:
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
Lm5:
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
Lm6:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) holds
(S-max (L~ z)) .. z < (W-min (L~ z)) .. z
Lm7:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) holds
(N-max (L~ z)) .. z < (W-min (L~ z)) .. z
Lm8:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) holds
(N-min (L~ z)) .. z < (W-min (L~ z)) .. z
Lm9:
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
Lm10:
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
theorem Th22: :: SPRECT_5:22
theorem :: SPRECT_5:23
theorem Th24: :: SPRECT_5:24
theorem Th25: :: SPRECT_5:25
theorem Th26: :: SPRECT_5:26
theorem Th27: :: SPRECT_5:27
theorem Th28: :: SPRECT_5:28
theorem :: SPRECT_5:29
theorem Th30: :: SPRECT_5:30
theorem :: SPRECT_5:31
Lm11:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = W-min (L~ z) holds
(E-max (L~ z)) .. z < (S-max (L~ z)) .. z
Lm12:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = W-min (L~ z) holds
(N-min (L~ z)) .. z < (E-max (L~ z)) .. z
Lm13:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = W-min (L~ z) holds
(N-min (L~ z)) .. z < (S-max (L~ z)) .. z
Lm14:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = W-min (L~ z) holds
(N-max (L~ z)) .. z < (S-max (L~ z)) .. z
Lm15:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = W-min (L~ z) holds
(W-max (L~ z)) .. z < (S-max (L~ z)) .. z
Lm16:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = W-min (L~ z) holds
(N-max (L~ z)) .. z < (E-min (L~ z)) .. z
Lm17:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = W-min (L~ z) holds
(N-min (L~ z)) .. z < (E-max (L~ z)) .. z
Lm18:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = W-min (L~ z) holds
(W-max (L~ z)) .. z < (E-max (L~ z)) .. z
Lm19:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = W-min (L~ z) holds
(W-max (L~ z)) .. z < (E-min (L~ z)) .. z
theorem Th32: :: SPRECT_5:32
theorem Th33: :: SPRECT_5:33
theorem Th34: :: SPRECT_5:34
theorem Th35: :: SPRECT_5:35
theorem Th36: :: SPRECT_5:36
theorem :: SPRECT_5:37
theorem Th38: :: SPRECT_5:38
theorem :: SPRECT_5:39
theorem Th40: :: SPRECT_5:40
theorem Th41: :: SPRECT_5:41
Lm20:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = S-max (L~ z) holds
(N-min (L~ z)) .. z < (E-max (L~ z)) .. z
Lm21:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = S-max (L~ z) holds
(W-max (L~ z)) .. z < (E-max (L~ z)) .. z
Lm22:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = S-max (L~ z) holds
(W-min (L~ z)) .. z < (E-max (L~ z)) .. z
Lm23:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = S-max (L~ z) holds
(W-max (L~ z)) .. z < (N-max (L~ z)) .. z
Lm24:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = S-max (L~ z) holds
(W-min (L~ z)) .. z < (N-min (L~ z)) .. z
Lm25:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = S-max (L~ z) holds
(S-min (L~ z)) .. z < (N-min (L~ z)) .. z
Lm26:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = S-max (L~ z) holds
(S-min (L~ z)) .. z < (N-max (L~ z)) .. z
theorem Th42: :: SPRECT_5:42
theorem Th43: :: SPRECT_5:43
theorem Th44: :: SPRECT_5:44
theorem :: SPRECT_5:45
theorem :: SPRECT_5:46
theorem :: SPRECT_5:47
theorem :: SPRECT_5:48
theorem :: SPRECT_5:49
theorem :: SPRECT_5:50
theorem :: SPRECT_5:51
theorem :: SPRECT_5:52
theorem :: SPRECT_5:53
theorem :: SPRECT_5:54
theorem :: SPRECT_5:55
Lm27:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = E-max (L~ z) holds
(S-max (L~ z)) .. z < (W-min (L~ z)) .. z
Lm28:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = E-max (L~ z) holds
(E-min (L~ z)) .. z < (W-min (L~ z)) .. z
Lm29:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = E-max (L~ z) holds
(E-min (L~ z)) .. z < (W-max (L~ z)) .. z
Lm30:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = E-max (L~ z) holds
(S-min (L~ z)) .. z < (W-max (L~ z)) .. z
theorem :: SPRECT_5:56
theorem :: SPRECT_5:57
theorem :: SPRECT_5:58
theorem :: SPRECT_5:59
theorem :: SPRECT_5:60
theorem :: SPRECT_5:61
theorem :: SPRECT_5:62
theorem :: SPRECT_5:63
theorem :: SPRECT_5:64
theorem :: SPRECT_5:65
theorem :: SPRECT_5:66
theorem :: SPRECT_5:67
theorem :: SPRECT_5:68
theorem :: SPRECT_5:69
theorem :: SPRECT_5:70
theorem :: SPRECT_5:71
theorem :: SPRECT_5:72
theorem :: SPRECT_5:73