:: The Lattice of Domains_of of a Topological Space
:: by Toshihiko Watanabe
::
:: Received June 12, 1992
:: Copyright (c) 1992 Association of Mizar Users
theorem Th1: :: TDLAT_1:1
theorem Th2: :: TDLAT_1:2
theorem Th3: :: TDLAT_1:3
theorem Th4: :: TDLAT_1:4
theorem Th5: :: TDLAT_1:5
theorem Th6: :: TDLAT_1:6
theorem Th7: :: TDLAT_1:7
theorem Th8: :: TDLAT_1:8
theorem Th9: :: TDLAT_1:9
theorem Th10: :: TDLAT_1:10
theorem :: TDLAT_1:11
theorem Th12: :: TDLAT_1:12
theorem :: TDLAT_1:13
theorem Th14: :: TDLAT_1:14
theorem Th15: :: TDLAT_1:15
theorem Th16: :: TDLAT_1:16
theorem Th17: :: TDLAT_1:17
theorem Th18: :: TDLAT_1:18
theorem Th19: :: TDLAT_1:19
theorem Th20: :: TDLAT_1:20
theorem Th21: :: TDLAT_1:21
theorem Th22: :: TDLAT_1:22
theorem Th23: :: TDLAT_1:23
theorem Th24: :: TDLAT_1:24
theorem Th25: :: TDLAT_1:25
theorem :: TDLAT_1:26
theorem :: TDLAT_1:27
theorem Th28: :: TDLAT_1:28
theorem Th29: :: TDLAT_1:29
:: deftheorem defines Domains_of TDLAT_1:def 1 :
:: deftheorem Def2 defines Domains_Union TDLAT_1:def 2 :
:: deftheorem Def3 defines Domains_Meet TDLAT_1:def 3 :
theorem Th30: :: TDLAT_1:30
:: deftheorem defines Domains_Lattice TDLAT_1:def 4 :
:: deftheorem defines Closed_Domains_of TDLAT_1:def 5 :
theorem :: TDLAT_1:31
:: deftheorem Def6 defines Closed_Domains_Union TDLAT_1:def 6 :
theorem Th32: :: TDLAT_1:32
:: deftheorem Def7 defines Closed_Domains_Meet TDLAT_1:def 7 :
theorem Th33: :: TDLAT_1:33
theorem Th34: :: TDLAT_1:34
:: deftheorem defines Closed_Domains_Lattice TDLAT_1:def 8 :
:: deftheorem defines Open_Domains_of TDLAT_1:def 9 :
theorem :: TDLAT_1:35
:: deftheorem Def10 defines Open_Domains_Union TDLAT_1:def 10 :
theorem Th36: :: TDLAT_1:36
:: deftheorem Def11 defines Open_Domains_Meet TDLAT_1:def 11 :
theorem Th37: :: TDLAT_1:37
theorem Th38: :: TDLAT_1:38
:: deftheorem defines Open_Domains_Lattice TDLAT_1:def 12 :
theorem Th39: :: TDLAT_1:39
theorem Th40: :: TDLAT_1:40
theorem :: TDLAT_1:41
theorem Th42: :: TDLAT_1:42
theorem Th43: :: TDLAT_1:43
theorem :: TDLAT_1:44