:: Components and Unions of Components
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received February 5, 1996
:: Copyright (c) 1996 Association of Mizar Users
:: deftheorem Def1 defines Component_of CONNSP_3:def 1 :
theorem Th1: :: CONNSP_3:1
theorem :: CONNSP_3:2
theorem Th3: :: CONNSP_3:3
theorem :: CONNSP_3:4
theorem Th5: :: CONNSP_3:5
theorem Th6: :: CONNSP_3:6
theorem Th7: :: CONNSP_3:7
theorem Th8: :: CONNSP_3:8
theorem :: CONNSP_3:9
theorem :: CONNSP_3:10
theorem Th11: :: CONNSP_3:11
theorem Th12: :: CONNSP_3:12
theorem Th13: :: CONNSP_3:13
theorem Th14: :: CONNSP_3:14
theorem Th15: :: CONNSP_3:15
theorem :: CONNSP_3:16
theorem :: CONNSP_3:17
theorem :: CONNSP_3:18
:: deftheorem Def2 defines a_union_of_components CONNSP_3:def 2 :
theorem Th19: :: CONNSP_3:19
theorem Th20: :: CONNSP_3:20
theorem Th21: :: CONNSP_3:21
theorem :: CONNSP_3:22
theorem :: CONNSP_3:23
theorem :: CONNSP_3:24
theorem :: CONNSP_3:25
:: deftheorem Def3 defines Down CONNSP_3:def 3 :
:: deftheorem defines Up CONNSP_3:def 4 :
:: deftheorem defines Down CONNSP_3:def 5 :
:: deftheorem defines Up CONNSP_3:def 6 :
:: deftheorem Def7 defines Component_of CONNSP_3:def 7 :
theorem :: CONNSP_3:26
theorem Th27: :: CONNSP_3:27
theorem :: CONNSP_3:28
canceled;
theorem :: CONNSP_3:29
theorem Th30: :: CONNSP_3:30
theorem :: CONNSP_3:31
theorem :: CONNSP_3:32
theorem :: CONNSP_3:33
theorem :: CONNSP_3:34
canceled;
theorem :: CONNSP_3:35
theorem :: CONNSP_3:36