:: On Kolmogorov Topological Spaces
:: by Zbigniew Karno
::
:: Received July 26, 1994
:: Copyright (c) 1994 Association of Mizar Users
:: deftheorem Def1 defines SubSpace TSP_1:def 1 :
theorem :: TSP_1:1
canceled;
theorem Th2: :: TSP_1:2
:: deftheorem Def2 defines SubSpace TSP_1:def 2 :
theorem :: TSP_1:3
canceled;
theorem Th4: :: TSP_1:4
:: deftheorem Def3 defines T_0 TSP_1:def 3 :
:: deftheorem Def4 defines T_0 TSP_1:def 4 :
Lm1:
for X being non empty non trivial anti-discrete TopStruct holds not X is T_0
Lm2:
for X being non empty TopSpace
for x being Point of X holds x in Cl {x}
:: deftheorem Def5 defines T_0 TSP_1:def 5 :
:: deftheorem Def6 defines T_0 TSP_1:def 6 :
:: deftheorem defines T_0 TSP_1:def 7 :
:: deftheorem Def8 defines T_0 TSP_1:def 8 :
:: deftheorem Def9 defines T_0 TSP_1:def 9 :
theorem :: TSP_1:5
theorem Th6: :: TSP_1:6
theorem Th7: :: TSP_1:7
theorem Th8: :: TSP_1:8
theorem Th9: :: TSP_1:9
theorem Th10: :: TSP_1:10
theorem Th11: :: TSP_1:11
theorem :: TSP_1:12
:: deftheorem Def10 defines T_0 TSP_1:def 10 :
:: deftheorem Def11 defines T_0 TSP_1:def 11 :
:: deftheorem defines T_0 TSP_1:def 12 :
theorem Th13: :: TSP_1:13
theorem :: TSP_1:14
:: deftheorem defines T_0 TSP_1:def 13 :
:: deftheorem Def14 defines T_0 TSP_1:def 14 :
theorem Th15: :: TSP_1:15
theorem :: TSP_1:16
theorem :: TSP_1:17
theorem :: TSP_1:18
theorem :: TSP_1:19
theorem :: TSP_1:20
theorem :: TSP_1:21