:: Topological Properties of Subsets in Real Numbers
:: by Konrad Raczkowski and Pawe{\l} Sadowski
::
:: Received June 18, 1990
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem defines [. RCOMP_1:def 1 :
:: deftheorem defines ]. RCOMP_1:def 2 :
theorem :: RCOMP_1:1
canceled;
theorem :: RCOMP_1:2
canceled;
theorem :: RCOMP_1:3
canceled;
theorem :: RCOMP_1:4
canceled;
theorem :: RCOMP_1:5
canceled;
theorem :: RCOMP_1:6
canceled;
theorem :: RCOMP_1:7
canceled;
theorem Th8: :: RCOMP_1:8
theorem :: RCOMP_1:9
theorem :: RCOMP_1:10
:: deftheorem Def3 defines compact RCOMP_1:def 3 :
:: deftheorem Def4 defines closed RCOMP_1:def 4 :
:: deftheorem Def5 defines open RCOMP_1:def 5 :
theorem :: RCOMP_1:11
canceled;
theorem :: RCOMP_1:12
canceled;
theorem :: RCOMP_1:13
canceled;
theorem :: RCOMP_1:14
canceled;
theorem :: RCOMP_1:15
canceled;
theorem :: RCOMP_1:16
canceled;
theorem :: RCOMP_1:17
canceled;
theorem :: RCOMP_1:18
canceled;
theorem :: RCOMP_1:19
canceled;
theorem :: RCOMP_1:20
canceled;
theorem :: RCOMP_1:21
canceled;
theorem Th22: :: RCOMP_1:22
theorem Th23: :: RCOMP_1:23
theorem :: RCOMP_1:24
theorem Th25: :: RCOMP_1:25
theorem Th26: :: RCOMP_1:26
theorem Th27: :: RCOMP_1:27
theorem Th28: :: RCOMP_1:28
theorem :: RCOMP_1:29
theorem Th30: :: RCOMP_1:30
theorem Th31: :: RCOMP_1:31
theorem :: RCOMP_1:32
theorem :: RCOMP_1:33
:: deftheorem RCOMP_1:def 6 :
canceled;
:: deftheorem Def7 defines Neighbourhood RCOMP_1:def 7 :
theorem :: RCOMP_1:34
canceled;
theorem :: RCOMP_1:35
canceled;
theorem :: RCOMP_1:36
canceled;
theorem :: RCOMP_1:37
theorem :: RCOMP_1:38
theorem Th39: :: RCOMP_1:39
theorem :: RCOMP_1:40
theorem :: RCOMP_1:41
theorem :: RCOMP_1:42
canceled;
theorem Th43: :: RCOMP_1:43
theorem Th44: :: RCOMP_1:44
theorem :: RCOMP_1:45
:: deftheorem defines [. RCOMP_1:def 8 :
:: deftheorem defines ]. RCOMP_1:def 9 :