:: The Ordering of Points on a Curve, Part {IV}
:: by Artur Korni{\l}owicz
::
:: Received September 16, 2002
:: Copyright (c) 2002 Association of Mizar Users
Lm1:
dom proj1 = the carrier of (TOP-REAL 2)
by FUNCT_2:def 1;
Lm2:
dom proj2 = the carrier of (TOP-REAL 2)
by FUNCT_2:def 1;
theorem :: JORDAN18:1
theorem :: JORDAN18:2
canceled;
theorem :: JORDAN18:3
theorem Th4: :: JORDAN18:4
theorem Th5: :: JORDAN18:5
theorem Th6: :: JORDAN18:6
theorem Th7: :: JORDAN18:7
theorem Th8: :: JORDAN18:8
theorem Th9: :: JORDAN18:9
theorem :: JORDAN18:10
theorem :: JORDAN18:11
theorem Th12: :: JORDAN18:12
theorem Th13: :: JORDAN18:13
theorem :: JORDAN18:14
theorem :: JORDAN18:15
theorem :: JORDAN18:16
canceled;
theorem :: JORDAN18:17
canceled;
theorem Th18: :: JORDAN18:18
:: deftheorem defines North-Bound JORDAN18:def 1 :
:: deftheorem defines South-Bound JORDAN18:def 2 :
theorem :: JORDAN18:19
canceled;
theorem :: JORDAN18:20
theorem :: JORDAN18:21
canceled;
theorem Th22: :: JORDAN18:22
theorem Th23: :: JORDAN18:23
theorem Th24: :: JORDAN18:24
theorem :: JORDAN18:25
theorem Th26: :: JORDAN18:26
theorem :: JORDAN18:27
theorem :: JORDAN18:28
:: deftheorem Def3 defines -separate JORDAN18:def 3 :
theorem :: JORDAN18:29
theorem :: JORDAN18:30
theorem :: JORDAN18:31
theorem Th32: :: JORDAN18:32
theorem Th33: :: JORDAN18:33
theorem Th34: :: JORDAN18:34
theorem Th35: :: JORDAN18:35
theorem :: JORDAN18:36
theorem :: JORDAN18:37
theorem :: JORDAN18:38