:: Compact Spaces
:: by Agata Darmochwa{\l}
::
:: Received September 19, 1989
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem COMPTS_1:def 1 :
canceled;
:: deftheorem COMPTS_1:def 2 :
canceled;
:: deftheorem Def3 defines compact COMPTS_1:def 3 :
:: deftheorem COMPTS_1:def 4 :
canceled;
:: deftheorem defines regular COMPTS_1:def 5 :
:: deftheorem defines normal COMPTS_1:def 6 :
:: deftheorem Def7 defines compact COMPTS_1:def 7 :
theorem :: COMPTS_1:1
canceled;
theorem :: COMPTS_1:2
canceled;
theorem :: COMPTS_1:3
canceled;
theorem :: COMPTS_1:4
canceled;
theorem :: COMPTS_1:5
canceled;
theorem :: COMPTS_1:6
canceled;
theorem :: COMPTS_1:7
canceled;
theorem :: COMPTS_1:8
canceled;
theorem :: COMPTS_1:9
canceled;
theorem Th10: :: COMPTS_1:10
theorem Th11: :: COMPTS_1:11
theorem Th12: :: COMPTS_1:12
theorem Th13: :: COMPTS_1:13
theorem :: COMPTS_1:14
theorem Th15: :: COMPTS_1:15
theorem Th16: :: COMPTS_1:16
theorem Th17: :: COMPTS_1:17
theorem Th18: :: COMPTS_1:18
theorem Th19: :: COMPTS_1:19
theorem :: COMPTS_1:20
theorem :: COMPTS_1:21
theorem :: COMPTS_1:22
theorem :: COMPTS_1:23
theorem Th24: :: COMPTS_1:24
theorem Th25: :: COMPTS_1:25
theorem :: COMPTS_1:26
:: deftheorem defines 1TopSp COMPTS_1:def 8 :
theorem Th27: :: COMPTS_1:27
theorem Th42: :: COMPTS_1:28
theorem :: COMPTS_1:29
theorem :: COMPTS_1:30