:: The Lattice of Domains of an Extremally Disconnected Space
:: by Zbigniew Karno
::
:: Received August 27, 1992
:: Copyright (c) 1992 Association of Mizar Users
theorem :: TDLAT_3:1
canceled;
theorem Th2: :: TDLAT_3:2
theorem Th3: :: TDLAT_3:3
theorem Th4: :: TDLAT_3:4
theorem :: TDLAT_3:5
canceled;
theorem :: TDLAT_3:6
theorem Th7: :: TDLAT_3:7
theorem :: TDLAT_3:8
theorem Th9: :: TDLAT_3:9
theorem Th10: :: TDLAT_3:10
theorem Th11: :: TDLAT_3:11
:: deftheorem Def1 defines discrete TDLAT_3:def 1 :
:: deftheorem Def2 defines anti-discrete TDLAT_3:def 2 :
theorem :: TDLAT_3:12
theorem Th13: :: TDLAT_3:13
theorem Th14: :: TDLAT_3:14
theorem Th15: :: TDLAT_3:15
theorem :: TDLAT_3:16
:: deftheorem Def3 defines almost_discrete TDLAT_3:def 3 :
theorem Th17: :: TDLAT_3:17
theorem Th18: :: TDLAT_3:18
theorem Th19: :: TDLAT_3:19
theorem Th20: :: TDLAT_3:20
theorem Th21: :: TDLAT_3:21
theorem :: TDLAT_3:22
theorem Th23: :: TDLAT_3:23
theorem Th24: :: TDLAT_3:24
theorem :: TDLAT_3:25
theorem :: TDLAT_3:26
theorem :: TDLAT_3:27
theorem :: TDLAT_3:28
:: deftheorem Def4 defines extremally_disconnected TDLAT_3:def 4 :
theorem Th29: :: TDLAT_3:29
theorem Th30: :: TDLAT_3:30
theorem :: TDLAT_3:31
theorem Th32: :: TDLAT_3:32
theorem :: TDLAT_3:33
theorem Th34: :: TDLAT_3:34
theorem Th35: :: TDLAT_3:35
theorem Th36: :: TDLAT_3:36
theorem :: TDLAT_3:37
theorem Th38: :: TDLAT_3:38
:: deftheorem Def5 defines hereditarily_extremally_disconnected TDLAT_3:def 5 :
theorem Th39: :: TDLAT_3:39
theorem :: TDLAT_3:40
theorem Th41: :: TDLAT_3:41
theorem Th42: :: TDLAT_3:42
theorem Th43: :: TDLAT_3:43
theorem Th44: :: TDLAT_3:44
theorem Th45: :: TDLAT_3:45
theorem Th46: :: TDLAT_3:46
theorem Th47: :: TDLAT_3:47
theorem :: TDLAT_3:48
theorem :: TDLAT_3:49
theorem :: TDLAT_3:50
theorem Th51: :: TDLAT_3:51
theorem :: TDLAT_3:52
theorem :: TDLAT_3:53
theorem :: TDLAT_3:54
theorem :: TDLAT_3:55