:: On the components of the complement of a special polygonal curve
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received January 21, 1999
:: Copyright (c) 1999 Association of Mizar Users
theorem Th1: :: SPRECT_4:1
theorem :: SPRECT_4:2
theorem :: SPRECT_4:3
canceled;
theorem Th4: :: SPRECT_4:4
theorem Th5: :: SPRECT_4:5
theorem Th6: :: SPRECT_4:6
Lm1:
for f being non constant standard clockwise_oriented special_circular_sequence st f /. 1 = N-min (L~ f) holds
LeftComp f <> RightComp f
Lm2:
for f being non constant standard special_circular_sequence st f /. 1 = N-min (L~ f) holds
LeftComp f <> RightComp f
theorem :: SPRECT_4:7