:: Connected Spaces
:: by Beata Padlewska
::
:: Received May 6, 1989
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem Def1 defines are_separated CONNSP_1:def 1 :
theorem :: CONNSP_1:1
canceled;
theorem Th2: :: CONNSP_1:2
theorem Th3: :: CONNSP_1:3
theorem Th4: :: CONNSP_1:4
theorem Th5: :: CONNSP_1:5
theorem Th6: :: CONNSP_1:6
theorem Th7: :: CONNSP_1:7
theorem Th8: :: CONNSP_1:8
theorem Th9: :: CONNSP_1:9
theorem Th10: :: CONNSP_1:10
:: deftheorem Def2 defines connected CONNSP_1:def 2 :
theorem Th11: :: CONNSP_1:11
theorem :: CONNSP_1:12
theorem Th13: :: CONNSP_1:13
theorem :: CONNSP_1:14
theorem :: CONNSP_1:15
:: deftheorem Def3 defines connected CONNSP_1:def 3 :
theorem Th16: :: CONNSP_1:16
theorem Th17: :: CONNSP_1:17
theorem Th18: :: CONNSP_1:18
theorem Th19: :: CONNSP_1:19
theorem Th20: :: CONNSP_1:20
theorem Th21: :: CONNSP_1:21
theorem :: CONNSP_1:22
theorem :: CONNSP_1:23
theorem Th24: :: CONNSP_1:24
theorem :: CONNSP_1:25
theorem Th26: :: CONNSP_1:26
theorem Th27: :: CONNSP_1:27
theorem Th28: :: CONNSP_1:28
theorem Th29: :: CONNSP_1:29
:: deftheorem Def4 defines are_joined CONNSP_1:def 4 :
theorem Th30: :: CONNSP_1:30
theorem Th31: :: CONNSP_1:31
theorem :: CONNSP_1:32
theorem Th33: :: CONNSP_1:33
:: deftheorem Def5 defines is_a_component_of CONNSP_1:def 5 :
theorem Th34: :: CONNSP_1:34
theorem :: CONNSP_1:35
theorem Th36: :: CONNSP_1:36
theorem :: CONNSP_1:37
theorem :: CONNSP_1:38
:: deftheorem Def6 defines is_a_component_of CONNSP_1:def 6 :
theorem :: CONNSP_1:39
:: deftheorem Def7 defines Component_of CONNSP_1:def 7 :
theorem Th40: :: CONNSP_1:40
theorem Th41: :: CONNSP_1:41
theorem Th42: :: CONNSP_1:42
theorem Th43: :: CONNSP_1:43
theorem :: CONNSP_1:44
theorem :: CONNSP_1:45
theorem :: CONNSP_1:46