:: TOPS_3 semantic presentation

theorem Th1: :: TOPS_3:1
for b1 being TopStruct
for b2 being Subset of b1 holds
( ( b2 = {} b1 implies b2 ` = [#] b1 ) & ( b2 ` = [#] b1 implies b2 = {} b1 ) & ( b2 = {} implies b2 ` = the carrier of b1 ) & ( b2 ` = the carrier of b1 implies b2 = {} ) )
proof end;

theorem Th2: :: TOPS_3:2
for b1 being TopStruct
for b2 being Subset of b1 holds
( ( b2 = [#] b1 implies b2 ` = {} b1 ) & ( b2 ` = {} b1 implies b2 = [#] b1 ) & ( b2 = the carrier of b1 implies b2 ` = {} ) & ( b2 ` = {} implies b2 = the carrier of b1 ) )
proof end;

theorem Th3: :: TOPS_3:3
for b1 being TopSpace
for b2, b3 being Subset of b1 holds (Int b2) /\ (Cl b3) c= Cl (b2 /\ b3)
proof end;

theorem Th4: :: TOPS_3:4
for b1 being TopSpace
for b2, b3 being Subset of b1 holds Int (b2 \/ b3) c= (Cl b2) \/ (Int b3)
proof end;

theorem Th5: :: TOPS_3:5
for b1 being TopSpace
for b2, b3 being Subset of b1 st b3 is closed holds
Int (b3 \/ b2) c= b3 \/ (Int b2)
proof end;

theorem Th6: :: TOPS_3:6
for b1 being TopSpace
for b2, b3 being Subset of b1 st b3 is closed holds
Int (b3 \/ b2) = Int (b3 \/ (Int b2))
proof end;

theorem Th7: :: TOPS_3:7
for b1 being TopSpace
for b2 being Subset of b1 st b2 misses Int (Cl b2) holds
Int (Cl b2) = {}
proof end;

theorem Th8: :: TOPS_3:8
for b1 being TopSpace
for b2 being Subset of b1 st b2 \/ (Cl (Int b2)) = the carrier of b1 holds
Cl (Int b2) = the carrier of b1
proof end;

definition
let c1 be TopStruct ;
let c2 be Subset of c1;
redefine attr a2 is boundary means :Def1: :: TOPS_3:def 1
 Int a2 = {} ;
compatibility
( c2 is boundary iff Int c2 = {} ) by TOPS_1:84;
end;

:: deftheorem Def1 defines boundary TOPS_3:def 1 :
for b1 being TopStruct
for b2 being Subset of b1 holds
( b2 is boundary iff Int b2 = {} );

theorem Th9: :: TOPS_3:9
for b1 being TopSpace holds {} b1 is boundary ;

theorem Th10: :: TOPS_3:10
for b1 being non empty TopSpace
for b2 being Subset of b1 st b2 is boundary holds
b2 <> the carrier of b1
proof end;

theorem Th11: :: TOPS_3:11
for b1 being TopSpace
for b2, b3 being Subset of b1 st b2 is boundary & b3 c= b2 holds
b3 is boundary
proof end;

theorem Th12: :: TOPS_3:12
for b1 being TopSpace
for b2 being Subset of b1 holds
( b2 is boundary iff for b3 being Subset of b1 st b2 ` c= b3 & b3 is closed holds
b3 = the carrier of b1 )
proof end;

theorem Th13: :: TOPS_3:13
for b1 being TopSpace
for b2 being Subset of b1 holds
( b2 is boundary iff for b3 being Subset of b1 st b3 <> {} & b3 is open holds
b2 ` meets b3 )
proof end;

theorem Th14: :: TOPS_3:14
for b1 being TopSpace
for b2 being Subset of b1 holds
( b2 is boundary iff for b3 being Subset of b1 st b3 is closed holds
Int b3 = Int (b3 \/ b2) )
proof end;

theorem Th15: :: TOPS_3:15
for b1 being TopSpace
for b2, b3 being Subset of b1 st ( b2 is boundary or b3 is boundary ) holds
b2 /\ b3 is boundary
proof end;

definition
let c1 be TopStruct ;
let c2 be Subset of c1;
redefine attr a2 is dense means :Def2: :: TOPS_3:def 2
 Cl a2 = the carrier of a1;
compatibility
( c2 is dense iff Cl c2 = the carrier of c1 )
proof end;
end;

:: deftheorem Def2 defines dense TOPS_3:def 2 :
for b1 being TopStruct
for b2 being Subset of b1 holds
( b2 is dense iff Cl b2 = the carrier of b1 );

theorem Th16: :: TOPS_3:16
for b1 being TopSpace holds [#] b1 is dense ;

theorem Th17: :: TOPS_3:17
for b1 being non empty TopSpace
for b2 being Subset of b1 st b2 is dense holds
b2 <> {}
proof end;

theorem Th18: :: TOPS_3:18
for b1 being non empty TopSpace
for b2 being Subset of b1 holds
( b2 is dense iff b2 ` is boundary )
proof end;

theorem Th19: :: TOPS_3:19
for b1 being non empty TopSpace
for b2 being Subset of b1 holds
( b2 is dense iff for b3 being Subset of b1 st b2 c= b3 & b3 is closed holds
b3 = the carrier of b1 )
proof end;

theorem Th20: :: TOPS_3:20
for b1 being non empty TopSpace
for b2 being Subset of b1 holds
( b2 is dense iff for b3 being Subset of b1 st b3 is open holds
Cl b3 = Cl (b3 /\ b2) )
proof end;

theorem Th21: :: TOPS_3:21
for b1 being non empty TopSpace
for b2, b3 being Subset of b1 st ( b2 is dense or b3 is dense ) holds
b2 \/ b3 is dense
proof end;

definition
let c1 be TopStruct ;
let c2 be Subset of c1;
redefine attr a2 is nowhere_dense means :Def3: :: TOPS_3:def 3
 Int (Cl a2) = {} ;
compatibility
( c2 is nowhere_dense iff Int (Cl c2) = {} )
proof end;
end;

:: deftheorem Def3 defines nowhere_dense TOPS_3:def 3 :
for b1 being TopStruct
for b2 being Subset of b1 holds
( b2 is nowhere_dense iff Int (Cl b2) = {} );

theorem Th22: :: TOPS_3:22
for b1 being non empty TopSpace holds {} b1 is nowhere_dense ;

theorem Th23: :: TOPS_3:23
for b1 being non empty TopSpace
for b2 being Subset of b1 st b2 is nowhere_dense holds
b2 <> the carrier of b1
proof end;

theorem Th24: :: TOPS_3:24
for b1 being non empty TopSpace
for b2 being Subset of b1 st b2 is nowhere_dense holds
Cl b2 is nowhere_dense
proof end;

theorem Th25: :: TOPS_3:25
for b1 being non empty TopSpace
for b2 being Subset of b1 st b2 is nowhere_dense holds
not b2 is dense
proof end;

theorem Th26: :: TOPS_3:26
for b1 being non empty TopSpace
for b2, b3 being Subset of b1 st b2 is nowhere_dense & b3 c= b2 holds
b3 is nowhere_dense
proof end;

theorem Th27: :: TOPS_3:27
for b1 being non empty TopSpace
for b2 being Subset of b1 holds
( b2 is nowhere_dense iff ex b3 being Subset of b1 st
( b2 c= b3 & b3 is closed & b3 is boundary ) )
proof end;

theorem Th28: :: TOPS_3:28
for b1 being non empty TopSpace
for b2 being Subset of b1 holds
( b2 is nowhere_dense iff for b3 being Subset of b1 st b3 <> {} & b3 is open holds
ex b4 being Subset of b1 st
( b4 c= b3 & b4 <> {} & b4 is open & b2 misses b4 ) )
proof end;

theorem Th29: :: TOPS_3:29
for b1 being non empty TopSpace
for b2, b3 being Subset of b1 st ( b2 is nowhere_dense or b3 is nowhere_dense ) holds
b2 /\ b3 is nowhere_dense
proof end;

theorem Th30: :: TOPS_3:30
for b1 being non empty TopSpace
for b2, b3 being Subset of b1 st b2 is nowhere_dense & b3 is boundary holds
b2 \/ b3 is boundary
proof end;

definition
let c1 be TopStruct ;
let c2 be Subset of c1;
attr a2 is everywhere_dense means :Def4: :: TOPS_3:def 4
 Cl (Int a2) = [#] a1;
end;

:: deftheorem Def4 defines everywhere_dense TOPS_3:def 4 :
for b1 being TopStruct
for b2 being Subset of b1 holds
( b2 is everywhere_dense iff Cl (Int b2) = [#] b1 );

definition
let c1 be TopStruct ;
let c2 be Subset of c1;
redefine attr a2 is everywhere_dense means :: TOPS_3:def 5
 Cl (Int a2) = the carrier of a1;
compatibility
( c2 is everywhere_dense iff Cl (Int c2) = the carrier of c1 )
proof end;
end;

:: deftheorem Def5 defines everywhere_dense TOPS_3:def 5 :
for b1 being TopStruct
for b2 being Subset of b1 holds
( b2 is everywhere_dense iff Cl (Int b2) = the carrier of b1 );

theorem Th31: :: TOPS_3:31
for b1 being non empty TopSpace holds [#] b1 is everywhere_dense
proof end;

theorem Th32: :: TOPS_3:32
for b1 being non empty TopSpace
for b2 being Subset of b1 st b2 is everywhere_dense holds
Int b2 is everywhere_dense
proof end;

theorem Th33: :: TOPS_3:33
for b1 being non empty TopSpace
for b2 being Subset of b1 st b2 is everywhere_dense holds
b2 is dense
proof end;

theorem Th34: :: TOPS_3:34
for b1 being non empty TopSpace
for b2 being Subset of b1 st b2 is everywhere_dense holds
b2 <> {}
proof end;

theorem Th35: :: TOPS_3:35
for b1 being non empty TopSpace
for b2 being Subset of b1 holds
( b2 is everywhere_dense iff Int b2 is dense )
proof end;

theorem Th36: :: TOPS_3:36
for b1 being non empty TopSpace
for b2 being Subset of b1 st b2 is open & b2 is dense holds
b2 is everywhere_dense
proof end;

theorem Th37: :: TOPS_3:37
for b1 being non empty TopSpace
for b2 being Subset of b1 st b2 is everywhere_dense holds
not b2 is boundary
proof end;

theorem Th38: :: TOPS_3:38
for b1 being non empty TopSpace
for b2, b3 being Subset of b1 st b2 is everywhere_dense & b2 c= b3 holds
b3 is everywhere_dense
proof end;

theorem Th39: :: TOPS_3:39
for b1 being non empty TopSpace
for b2 being Subset of b1 holds
( b2 is everywhere_dense iff b2 ` is nowhere_dense )
proof end;

theorem Th40: :: TOPS_3:40
for b1 being non empty TopSpace
for b2 being Subset of b1 holds
( b2 is nowhere_dense iff b2 ` is everywhere_dense )
proof end;

theorem Th41: :: TOPS_3:41
for b1 being non empty TopSpace
for b2 being Subset of b1 holds
( b2 is everywhere_dense iff ex b3 being Subset of b1 st
( b3 c= b2 & b3 is open & b3 is dense ) )
proof end;

theorem Th42: :: TOPS_3:42
for b1 being non empty TopSpace
for b2 being Subset of b1 holds
( b2 is everywhere_dense iff for b3 being Subset of b1 st b3 <> the carrier of b1 & b3 is closed holds
ex b4 being Subset of b1 st
( b3 c= b4 & b4 <> the carrier of b1 & b4 is closed & b2 \/ b4 = the carrier of b1 ) )
proof end;

theorem Th43: :: TOPS_3:43
for b1 being non empty TopSpace
for b2, b3 being Subset of b1 st ( b2 is everywhere_dense or b3 is everywhere_dense ) holds
b2 \/ b3 is everywhere_dense
proof end;

theorem Th44: :: TOPS_3:44
for b1 being non empty TopSpace
for b2, b3 being Subset of b1 st b2 is everywhere_dense & b3 is everywhere_dense holds
b2 /\ b3 is everywhere_dense
proof end;

theorem Th45: :: TOPS_3:45
for b1 being non empty TopSpace
for b2, b3 being Subset of b1 st b2 is everywhere_dense & b3 is dense holds
b2 /\ b3 is dense
proof end;

theorem Th46: :: TOPS_3:46
for b1 being non empty TopSpace
for b2, b3 being Subset of b1 st b2 is dense & b3 is nowhere_dense holds
b2 \ b3 is dense
proof end;

theorem Th47: :: TOPS_3:47
for b1 being non empty TopSpace
for b2, b3 being Subset of b1 st b2 is everywhere_dense & b3 is boundary holds
b2 \ b3 is dense
proof end;

theorem Th48: :: TOPS_3:48
for b1 being non empty TopSpace
for b2, b3 being Subset of b1 st b2 is everywhere_dense & b3 is nowhere_dense holds
b2 \ b3 is everywhere_dense
proof end;

theorem Th49: :: TOPS_3:49
for b1 being non empty TopSpace
for b2 being Subset of b1 st b2 is everywhere_dense holds
ex b3, b4 being Subset of b1 st
( b3 is open & b3 is dense & b4 is nowhere_dense & b3 \/ b4 = b2 & b3 misses b4 )
proof end;

theorem Th50: :: TOPS_3:50
for b1 being non empty TopSpace
for b2 being Subset of b1 st b2 is everywhere_dense holds
ex b3, b4 being Subset of b1 st
( b3 is open & b3 is dense & b4 is closed & b4 is boundary & b3 \/ (b2 /\ b4) = b2 & b3 misses b4 & b3 \/ b4 = the carrier of b1 )
proof end;

theorem Th51: :: TOPS_3:51
for b1 being non empty TopSpace
for b2 being Subset of b1 st b2 is nowhere_dense holds
ex b3, b4 being Subset of b1 st
( b3 is closed & b3 is boundary & b4 is everywhere_dense & b3 /\ b4 = b2 & b3 \/ b4 = the carrier of b1 )
proof end;

theorem Th52: :: TOPS_3:52
for b1 being non empty TopSpace
for b2 being Subset of b1 st b2 is nowhere_dense holds
ex b3, b4 being Subset of b1 st
( b3 is closed & b3 is boundary & b4 is open & b4 is dense & b3 /\ (b2 \/ b4) = b2 & b3 misses b4 & b3 \/ b4 = the carrier of b1 )
proof end;

theorem Th53: :: TOPS_3:53
for b1 being non empty TopSpace
for b2 being SubSpace of b1
for b3 being Subset of b1
for b4 being Subset of b2 st b4 c= b3 holds
Cl b4 c= Cl b3
proof end;

theorem Th54: :: TOPS_3:54
for b1 being non empty TopSpace
for b2 being SubSpace of b1
for b3, b4 being Subset of b1
for b5 being Subset of b2 st b3 is closed & b3 c= the carrier of b2 & b4 c= b3 & b4 = b5 holds
Cl b4 = Cl b5
proof end;

theorem Th55: :: TOPS_3:55
for b1 being non empty TopSpace
for b2 being non empty closed SubSpace of b1
for b3 being Subset of b1
for b4 being Subset of b2 st b3 = b4 holds
Cl b3 = Cl b4
proof end;

theorem Th56: :: TOPS_3:56
for b1 being non empty TopSpace
for b2 being SubSpace of b1
for b3 being Subset of b1
for b4 being Subset of b2 st b3 c= b4 holds
Int b3 c= Int b4
proof end;

theorem Th57: :: TOPS_3:57
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 c= the carrier of b2 & b4 c= b3 & b4 = b5 holds
Int b4 = Int b5
proof end;

theorem Th58: :: TOPS_3:58
for b1 being non empty TopSpace
for b2 being non empty open SubSpace of b1
for b3 being Subset of b1
for b4 being Subset of b2 st b3 = b4 holds
Int b3 = Int b4
proof end;

theorem Th59: :: TOPS_3:59
for b1 being non empty TopSpace
for b2 being SubSpace of b1
for b3 being Subset of b1
for b4 being Subset of b2 st b3 c= b4 & b3 is dense holds
b4 is dense
proof end;

theorem Th60: :: TOPS_3:60
for b1 being non empty TopSpace
for b2 being SubSpace of b1
for b3, b4 being Subset of b1
for b5 being Subset of b2 st b3 c= the carrier of b2 & b4 c= b3 & b4 = b5 holds
( ( b3 is dense & b5 is dense ) iff b4 is dense )
proof end;

theorem Th61: :: TOPS_3:61
for b1 being non empty TopSpace
for b2 being non empty SubSpace of b1
for b3 being Subset of b1
for b4 being Subset of b2 st b3 c= b4 & b3 is everywhere_dense holds
b4 is everywhere_dense
proof end;

theorem Th62: :: TOPS_3:62
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 c= the carrier of b2 & b4 c= b3 & b4 = b5 holds
( ( b3 is dense & b5 is everywhere_dense ) iff b4 is everywhere_dense )
proof end;

theorem Th63: :: TOPS_3:63
for b1 being non empty TopSpace
for b2 being non empty open SubSpace of b1
for b3, b4 being Subset of b1
for b5 being Subset of b2 st b4 = the carrier of b2 & b3 = b5 holds
( ( b4 is dense & b5 is everywhere_dense ) iff b3 is everywhere_dense )
proof end;

theorem Th64: :: TOPS_3:64
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 c= the carrier of b2 & b4 c= b3 & b4 = b5 holds
( ( b3 is everywhere_dense & b5 is everywhere_dense ) iff b4 is everywhere_dense )
proof end;

theorem Th65: :: TOPS_3:65
for b1 being non empty TopSpace
for b2 being non empty SubSpace of b1
for b3 being Subset of b1
for b4 being Subset of b2 st b3 c= b4 & b4 is boundary holds
b3 is boundary
proof end;

theorem Th66: :: TOPS_3:66
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 c= the carrier of b2 & b4 c= b3 & b4 = b5 & b4 is boundary holds
b5 is boundary
proof end;

theorem Th67: :: TOPS_3:67
for b1 being non empty TopSpace
for b2 being non empty open SubSpace of b1
for b3 being Subset of b1
for b4 being Subset of b2 st b3 = b4 holds
( b3 is boundary iff b4 is boundary )
proof end;

theorem Th68: :: TOPS_3:68
for b1 being non empty TopSpace
for b2 being non empty SubSpace of b1
for b3 being Subset of b1
for b4 being Subset of b2 st b3 c= b4 & b4 is nowhere_dense holds
b3 is nowhere_dense
proof end;

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
proof end;

theorem Th69: :: TOPS_3:69
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 c= the carrier of b2 & b4 c= b3 & b4 = b5 & b4 is nowhere_dense holds
b5 is nowhere_dense
proof end;

theorem Th70: :: TOPS_3:70
for b1 being non empty TopSpace
for b2 being non empty open SubSpace of b1
for b3 being Subset of b1
for b4 being Subset of b2 st b3 = b4 holds
( b3 is nowhere_dense iff b4 is nowhere_dense )
proof end;

theorem Th71: :: TOPS_3:71
for b1, b2 being 1-sorted st the carrier of b1 = the carrier of b2 holds
for b3 being Subset of b1
for b4 being Subset of b2 holds
( b3 = b4 iff b3 ` = b4 ` )
proof end;

theorem Th72: :: TOPS_3:72
for b1, b2 being TopStruct st the carrier of b1 = the carrier of b2 & ( for b3 being Subset of b1
for b4 being Subset of b2 st b3 = b4 holds
( b3 is open iff b4 is open ) ) holds
TopStruct(# the carrier of b1,the topology of b1 #) = TopStruct(# the carrier of b2,the topology of b2 #)
proof end;

theorem Th73: :: TOPS_3:73
for b1, b2 being TopStruct st the carrier of b1 = the carrier of b2 & ( for b3 being Subset of b1
for b4 being Subset of b2 st b3 = b4 holds
( b3 is closed iff b4 is closed ) ) holds
TopStruct(# the carrier of b1,the topology of b1 #) = TopStruct(# the carrier of b2,the topology of b2 #)
proof end;

theorem Th74: :: TOPS_3:74
for b1, b2 being TopSpace st the carrier of b1 = the carrier of b2 & ( for b3 being Subset of b1
for b4 being Subset of b2 st b3 = b4 holds
Int b3 = Int b4 ) holds
TopStruct(# the carrier of b1,the topology of b1 #) = TopStruct(# the carrier of b2,the topology of b2 #)
proof end;

theorem Th75: :: TOPS_3:75
for b1, b2 being TopSpace st the carrier of b1 = the carrier of b2 & ( for b3 being Subset of b1
for b4 being Subset of b2 st b3 = b4 holds
Cl b3 = Cl b4 ) holds
TopStruct(# the carrier of b1,the topology of b1 #) = TopStruct(# the carrier of b2,the topology of b2 #)
proof end;

theorem Th76: :: TOPS_3:76
for b1, b2 being TopSpace
for b3 being Subset of b1
for b4 being Subset of b2 st b3 = b4 & TopStruct(# the carrier of b1,the topology of b1 #) = TopStruct(# the carrier of b2,the topology of b2 #) & b3 is open holds
b4 is open
proof end;

theorem Th77: :: TOPS_3:77
for b1, b2 being TopSpace
for b3 being Subset of b1
for b4 being Subset of b2 st b3 = b4 & TopStruct(# the carrier of b1,the topology of b1 #) = TopStruct(# the carrier of b2,the topology of b2 #) holds
Int b3 = Int b4
proof end;

theorem Th78: :: TOPS_3:78
for b1, b2 being TopSpace
for b3 being Subset of b1
for b4 being Subset of b2 st b3 c= b4 & TopStruct(# the carrier of b1,the topology of b1 #) = TopStruct(# the carrier of b2,the topology of b2 #) holds
Int b3 c= Int b4
proof end;

theorem Th79: :: TOPS_3:79
for b1, b2 being TopSpace
for b3 being Subset of b1
for b4 being Subset of b2 st b3 = b4 & TopStruct(# the carrier of b1,the topology of b1 #) = TopStruct(# the carrier of b2,the topology of b2 #) & b3 is closed holds
b4 is closed
proof end;

theorem Th80: :: TOPS_3:80
for b1, b2 being TopSpace
for b3 being Subset of b1
for b4 being Subset of b2 st b3 = b4 & TopStruct(# the carrier of b1,the topology of b1 #) = TopStruct(# the carrier of b2,the topology of b2 #) holds
Cl b3 = Cl b4
proof end;

theorem Th81: :: TOPS_3:81
for b1, b2 being TopSpace
for b3 being Subset of b1
for b4 being Subset of b2 st b3 c= b4 & TopStruct(# the carrier of b1,the topology of b1 #) = TopStruct(# the carrier of b2,the topology of b2 #) holds
Cl b3 c= Cl b4
proof end;

theorem Th82: :: TOPS_3:82
for b1, b2 being TopSpace
for b3 being Subset of b1
for b4 being Subset of b2 st b4 c= b3 & TopStruct(# the carrier of b1,the topology of b1 #) = TopStruct(# the carrier of b2,the topology of b2 #) & b3 is boundary holds
b4 is boundary
proof end;

theorem Th83: :: TOPS_3:83
for b1, b2 being TopSpace
for b3 being Subset of b1
for b4 being Subset of b2 st b3 c= b4 & TopStruct(# the carrier of b1,the topology of b1 #) = TopStruct(# the carrier of b2,the topology of b2 #) & b3 is dense holds
b4 is dense
proof end;

theorem Th84: :: TOPS_3:84
for b1, b2 being TopSpace
for b3 being Subset of b1
for b4 being Subset of b2 st b4 c= b3 & TopStruct(# the carrier of b1,the topology of b1 #) = TopStruct(# the carrier of b2,the topology of b2 #) & b3 is nowhere_dense holds
b4 is nowhere_dense
proof end;

theorem Th85: :: TOPS_3:85
for b1, b2 being non empty TopSpace
for b3 being Subset of b1
for b4 being Subset of b2 st b3 c= b4 & TopStruct(# the carrier of b1,the topology of b1 #) = TopStruct(# the carrier of b2,the topology of b2 #) & b3 is everywhere_dense holds
b4 is everywhere_dense
proof end;