:: TOPS_3 semantic presentation
theorem Th1: :: TOPS_3:1
theorem Th2: :: TOPS_3:2
theorem Th3: :: TOPS_3:3
theorem Th4: :: TOPS_3:4
theorem Th5: :: TOPS_3:5
theorem Th6: :: TOPS_3:6
theorem Th7: :: TOPS_3:7
theorem Th8: :: TOPS_3:8
:: deftheorem Def1 defines boundary TOPS_3:def 1 :
theorem Th9: :: TOPS_3:9
theorem Th10: :: TOPS_3:10
theorem Th11: :: TOPS_3:11
theorem Th12: :: TOPS_3:12
theorem Th13: :: TOPS_3:13
theorem Th14: :: TOPS_3:14
theorem Th15: :: TOPS_3:15
:: deftheorem Def2 defines dense TOPS_3:def 2 :
theorem Th16: :: TOPS_3:16
theorem Th17: :: TOPS_3:17
theorem Th18: :: TOPS_3:18
theorem Th19: :: TOPS_3:19
theorem Th20: :: TOPS_3:20
theorem Th21: :: TOPS_3:21
:: deftheorem Def3 defines nowhere_dense TOPS_3:def 3 :
theorem Th22: :: TOPS_3:22
theorem Th23: :: TOPS_3:23
theorem Th24: :: TOPS_3:24
theorem Th25: :: TOPS_3:25
theorem Th26: :: TOPS_3:26
theorem Th27: :: TOPS_3:27
theorem Th28: :: TOPS_3:28
theorem Th29: :: TOPS_3:29
theorem Th30: :: TOPS_3:30
:: deftheorem Def4 defines everywhere_dense TOPS_3:def 4 :
:: deftheorem Def5 defines everywhere_dense TOPS_3:def 5 :
theorem Th31: :: TOPS_3:31
theorem Th32: :: TOPS_3:32
theorem Th33: :: TOPS_3:33
theorem Th34: :: TOPS_3:34
theorem Th35: :: TOPS_3:35
theorem Th36: :: TOPS_3:36
theorem Th37: :: TOPS_3:37
theorem Th38: :: TOPS_3:38
theorem Th39: :: TOPS_3:39
theorem Th40: :: TOPS_3:40
theorem Th41: :: TOPS_3:41
theorem Th42: :: TOPS_3:42
theorem Th43: :: TOPS_3:43
theorem Th44: :: TOPS_3:44
theorem Th45: :: TOPS_3:45
theorem Th46: :: TOPS_3:46
theorem Th47: :: TOPS_3:47
theorem Th48: :: TOPS_3:48
theorem Th49: :: TOPS_3:49
theorem Th50: :: TOPS_3:50
theorem Th51: :: TOPS_3:51
theorem Th52: :: TOPS_3:52
theorem Th53: :: TOPS_3:53
theorem Th54: :: TOPS_3:54
theorem Th55: :: TOPS_3:55
theorem Th56: :: TOPS_3:56
theorem Th57: :: TOPS_3:57
theorem Th58: :: TOPS_3:58
theorem Th59: :: TOPS_3:59
theorem Th60: :: TOPS_3:60
theorem Th61: :: TOPS_3:61
theorem Th62: :: TOPS_3:62
theorem Th63: :: TOPS_3:63
theorem Th64: :: TOPS_3:64
theorem Th65: :: TOPS_3:65
theorem Th66: :: TOPS_3:66
theorem Th67: :: TOPS_3:67
theorem Th68: :: TOPS_3:68
Lemma41:
for b1 being non empty TopSpace
for b2 being non empty SubSpace of b1
for b3, b4 being Subset of b1
for b5 being Subset of b2 st b3 is open & b3 = the carrier of b2 & b4 c= b3 & b4 = b5 & b4 is nowhere_dense holds
b5 is nowhere_dense
theorem Th69: :: TOPS_3:69
theorem Th70: :: TOPS_3:70
theorem Th71: :: TOPS_3:71
theorem Th72: :: TOPS_3:72
theorem Th73: :: TOPS_3:73
theorem Th74: :: TOPS_3:74
theorem Th75: :: TOPS_3:75
theorem Th76: :: TOPS_3:76
theorem Th77: :: TOPS_3:77
theorem Th78: :: TOPS_3:78
theorem Th79: :: TOPS_3:79
theorem Th80: :: TOPS_3:80
theorem Th81: :: TOPS_3:81
theorem Th82: :: TOPS_3:82
theorem Th83: :: TOPS_3:83
theorem Th84: :: TOPS_3:84
theorem Th85: :: TOPS_3:85