:: TOPS_1 semantic presentation

theorem Th1: :: TOPS_1:1

canceled;

theorem Th2: :: TOPS_1:2

for b₁ being 1-sorted
for b₂ being Subset of b₁ holds b₂ \/ ([#] b₁) = [#] b₁

proof end;

theorem Th3: :: TOPS_1:3

canceled;

theorem Th4: :: TOPS_1:4

canceled;

theorem Th5: :: TOPS_1:5

canceled;

theorem Th6: :: TOPS_1:6

canceled;

theorem Th7: :: TOPS_1:7

canceled;

theorem Th8: :: TOPS_1:8

for b₁ being 1-sorted holds ([#] b₁) ` = {} b₁

proof end;

theorem Th9: :: TOPS_1:9

canceled;

theorem Th10: :: TOPS_1:10

canceled;

theorem Th11: :: TOPS_1:11

canceled;

theorem Th12: :: TOPS_1:12

canceled;

theorem Th13: :: TOPS_1:13

canceled;

theorem Th14: :: TOPS_1:14

canceled;

theorem Th15: :: TOPS_1:15

canceled;

theorem Th16: :: TOPS_1:16

canceled;

theorem Th17: :: TOPS_1:17

canceled;

theorem Th18: :: TOPS_1:18

canceled;

theorem Th19: :: TOPS_1:19

canceled;

theorem Th20: :: TOPS_1:20

for b₁ being 1-sorted
for b₂, b₃ being Subset of b₁ holds
( b₂ c= b₃ iff b₂ misses b₃ ` )

proof end;

theorem Th21: :: TOPS_1:21

for b₁ being 1-sorted
for b₂, b₃ being Subset of b₁ st b₂ ` = b₃ ` holds
b₂ = b₃

proof end;

theorem Th22: :: TOPS_1:22

for b₁ being TopSpace holds {} b₁ is closed

proof end;

registration

let c₁ be TopSpace;
cluster {} a₁ -> closed ;
coherence by Th22;

end;

theorem Th23: :: TOPS_1:23

canceled;

theorem Th24: :: TOPS_1:24

canceled;

theorem Th25: :: TOPS_1:25

canceled;

theorem Th26: :: TOPS_1:26

for b₁ being TopStruct
for b₂ being Subset of b₁ holds Cl (Cl b₂) = Cl b₂

proof end;

theorem Th27: :: TOPS_1:27

for b₁ being TopStruct holds Cl ([#] b₁) = [#] b₁

proof end;

Lemma7: for b₁ being TopSpace
for b₂ being Subset of b₁ holds Cl b₂ is closed

proof end;

registration

let c₁ be TopSpace;
let c₂ be Subset of c₁;
cluster Cl a₂ -> closed ;
coherence by Lemma7;

end;

theorem Th28: :: TOPS_1:28

canceled;

theorem Th29: :: TOPS_1:29

for b₁ being TopStruct
for b₂ being Subset of b₁ holds
( b₂ is closed iff b₂ ` is open )

proof end;

registration

let c₁ be TopSpace;
let c₂ be closed Subset of c₁;
cluster a₂ ` -> open ;
coherence by Th29;

end;

theorem Th30: :: TOPS_1:30

for b₁ being TopStruct
for b₂ being Subset of b₁ holds
( b₂ is open iff b₂ ` is closed )

proof end;

registration

let c₁ be TopSpace;
cluster open Element of K10(the carrier of a₁);
existence

proof end;

end;

registration

let c₁ be TopSpace;
let c₂ be open Subset of c₁;
cluster a₂ ` -> closed ;
coherence by Th30;

end;

theorem Th31: :: TOPS_1:31

for b₁ being TopStruct
for b₂, b₃ being Subset of b₁ st b₂ is closed & b₃ c= b₂ holds
Cl b₃ c= b₂

proof end;

theorem Th32: :: TOPS_1:32

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ holds (Cl b₂) \ (Cl b₃) c= Cl (b₂ \ b₃)

proof end;

theorem Th33: :: TOPS_1:33

canceled;

theorem Th34: :: TOPS_1:34

for b₁ being TopStruct
for b₂, b₃ being Subset of b₁ st b₂ is closed & b₃ is closed holds
Cl (b₂ /\ b₃) = (Cl b₂) /\ (Cl b₃)

proof end;

theorem Th35: :: TOPS_1:35

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is closed & b₃ is closed holds
b₂ /\ b₃ is closed

proof end;

theorem Th36: :: TOPS_1:36

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is closed & b₃ is closed holds
b₂ \/ b₃ is closed

proof end;

theorem Th37: :: TOPS_1:37

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is open & b₃ is open holds
b₂ \/ b₃ is open

proof end;

theorem Th38: :: TOPS_1:38

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is open & b₃ is open holds
b₂ /\ b₃ is open

proof end;

Lemma15: for b₁ being non empty 1-sorted
for b₂ being Subset of b₁
for b₃ being Element of b₁ holds
( b₃ in b₂ ` iff not b₃ in b₂ )
by SUBSET_1:50, SUBSET_1:54;

theorem Th39: :: TOPS_1:39

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being Point of b₁ holds
( b₃ in Cl b₂ iff for b₄ being Subset of b₁ st b₄ is open & b₃ in b₄ holds
b₂ meets b₄ )

proof end;

theorem Th40: :: TOPS_1:40

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is open holds
b₂ /\ (Cl b₃) c= Cl (b₂ /\ b₃)

proof end;

theorem Th41: :: TOPS_1:41

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is open holds
Cl (b₂ /\ (Cl b₃)) = Cl (b₂ /\ b₃)

proof end;

definition

let c₁ be TopStruct ;
let c₂ be Subset of c₁;
func Int c₂ -> Subset of a₁ equals :: TOPS_1:def 1
(Cl (a₂ ` )) ` ;
coherence ;

end;

:: deftheorem Def1 defines Int TOPS_1:def 1 :

theorem Th42: :: TOPS_1:42

canceled;

theorem Th43: :: TOPS_1:43

for b₁ being TopSpace holds Int ([#] b₁) = [#] b₁

proof end;

theorem Th44: :: TOPS_1:44

for b₁ being TopStruct
for b₂ being Subset of b₁ holds Int b₂ c= b₂

proof end;

theorem Th45: :: TOPS_1:45

for b₁ being TopStruct
for b₂ being Subset of b₁ holds Int (Int b₂) = Int b₂ by Th26;

theorem Th46: :: TOPS_1:46

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ holds (Int b₂) /\ (Int b₃) = Int (b₂ /\ b₃)

proof end;

theorem Th47: :: TOPS_1:47

for b₁ being TopStruct holds Int ({} b₁) = {} b₁

proof end;

registration

let c₁ be TopStruct ;
cluster Int ({} a₁) -> empty ;
coherence by Th47;

end;

theorem Th48: :: TOPS_1:48

for b₁ being TopStruct
for b₂, b₃ being Subset of b₁ st b₂ c= b₃ holds
Int b₂ c= Int b₃

proof end;

theorem Th49: :: TOPS_1:49

for b₁ being TopStruct
for b₂, b₃ being Subset of b₁ holds (Int b₂) \/ (Int b₃) c= Int (b₂ \/ b₃)

proof end;

theorem Th50: :: TOPS_1:50

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ holds Int (b₂ \ b₃) c= (Int b₂) \ (Int b₃)

proof end;

theorem Th51: :: TOPS_1:51

for b₁ being TopSpace
for b₂ being Subset of b₁ holds Int b₂ is open ;

registration

let c₁ be TopSpace;
let c₂ be Subset of c₁;
cluster Int a₂ -> open ;
coherence ;

end;

theorem Th52: :: TOPS_1:52

for b₁ being TopSpace holds {} b₁ is open

proof end;

theorem Th53: :: TOPS_1:53

for b₁ being TopSpace holds [#] b₁ is open

proof end;

registration

let c₁ be TopSpace;
cluster {} a₁ -> open closed ;
coherence by Th52;
cluster [#] a₁ -> open ;
coherence by Th53;

end;

registration

let c₁ be TopSpace;
cluster empty -> open closed Element of K10(the carrier of a₁);
coherence

proof end;

end;

registration

let c₁ be TopSpace;
cluster open closed Element of K10(the carrier of a₁);
existence

proof end;

end;

registration

let c₁ be non empty TopSpace;
cluster non empty open closed Element of K10(the carrier of a₁);
existence

proof end;

end;

theorem Th54: :: TOPS_1:54

for b₁ being TopSpace
for b₂ being set
for b₃ being Subset of b₁ holds
( b₂ in Int b₃ iff ex b₄ being Subset of b₁ st
( b₄ is open & b₄ c= b₃ & b₂ in b₄ ) )

proof end;

theorem Th55: :: TOPS_1:55

for b₁ being TopSpace
for b₂ being TopStruct
for b₃ being Subset of b₁
for b₄ being Subset of b₂ holds
( ( b₄ is open implies Int b₄ = b₄ ) & ( Int b₃ = b₃ implies b₃ is open ) )

proof end;

theorem Th56: :: TOPS_1:56

for b₁ being TopStruct
for b₂, b₃ being Subset of b₁ st b₂ is open & b₂ c= b₃ holds
b₂ c= Int b₃

proof end;

theorem Th57: :: TOPS_1:57

for b₁ being TopSpace
for b₂ being Subset of b₁ holds
( b₂ is open iff for b₃ being set holds
( b₃ in b₂ iff ex b₄ being Subset of b₁ st
( b₄ is open & b₄ c= b₂ & b₃ in b₄ ) ) )

proof end;

theorem Th58: :: TOPS_1:58

for b₁ being TopStruct
for b₂ being Subset of b₁ holds Cl (Int b₂) = Cl (Int (Cl (Int b₂)))

proof end;

theorem Th59: :: TOPS_1:59

for b₁ being TopStruct
for b₂ being Subset of b₁ st b₂ is open holds
Cl (Int (Cl b₂)) = Cl b₂

proof end;

definition

let c₁ be TopStruct ;
let c₂ be Subset of c₁;
func Fr c₂ -> Subset of a₁ equals :: TOPS_1:def 2
(Cl a₂) /\ (Cl (a₂ ` ));
coherence ;

end;

:: deftheorem Def2 defines Fr TOPS_1:def 2 :

theorem Th60: :: TOPS_1:60

canceled;

theorem Th61: :: TOPS_1:61

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being Point of b₁ holds
( b₃ in Fr b₂ iff for b₄ being Subset of b₁ st b₄ is open & b₃ in b₄ holds
( b₂ meets b₄ & b₂ ` meets b₄ ) )

proof end;

theorem Th62: :: TOPS_1:62

for b₁ being TopStruct
for b₂ being Subset of b₁ holds Fr b₂ = Fr (b₂ ` ) ;

theorem Th63: :: TOPS_1:63

for b₁ being TopStruct
for b₂ being Subset of b₁ holds Fr b₂ c= Cl b₂ by XBOOLE_1:17;

theorem Th64: :: TOPS_1:64

for b₁ being TopStruct
for b₂ being Subset of b₁ holds Fr b₂ = ((Cl (b₂ ` )) /\ b₂) \/ ((Cl b₂) \ b₂)

proof end;

theorem Th65: :: TOPS_1:65

for b₁ being TopStruct
for b₂ being Subset of b₁ holds Cl b₂ = b₂ \/ (Fr b₂)

proof end;

theorem Th66: :: TOPS_1:66

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ holds Fr (b₂ /\ b₃) c= (Fr b₂) \/ (Fr b₃)

proof end;

theorem Th67: :: TOPS_1:67

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ holds Fr (b₂ \/ b₃) c= (Fr b₂) \/ (Fr b₃)

proof end;

theorem Th68: :: TOPS_1:68

for b₁ being TopStruct
for b₂ being Subset of b₁ holds Fr (Fr b₂) c= Fr b₂

proof end;

theorem Th69: :: TOPS_1:69

for b₁ being TopStruct
for b₂ being Subset of b₁ st b₂ is closed holds
Fr b₂ c= b₂

proof end;

Lemma36: for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ holds Fr b₂ c= ((Fr (b₂ \/ b₃)) \/ (Fr (b₂ /\ b₃))) \/ ((Fr b₂) /\ (Fr b₃))

proof end;

theorem Th70: :: TOPS_1:70

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ holds (Fr b₂) \/ (Fr b₃) = ((Fr (b₂ \/ b₃)) \/ (Fr (b₂ /\ b₃))) \/ ((Fr b₂) /\ (Fr b₃))

proof end;

theorem Th71: :: TOPS_1:71

for b₁ being TopStruct
for b₂ being Subset of b₁ holds Fr (Int b₂) c= Fr b₂

proof end;

theorem Th72: :: TOPS_1:72

for b₁ being TopStruct
for b₂ being Subset of b₁ holds Fr (Cl b₂) c= Fr b₂

proof end;

theorem Th73: :: TOPS_1:73

for b₁ being TopStruct
for b₂ being Subset of b₁ holds Int b₂ misses Fr b₂

proof end;

theorem Th74: :: TOPS_1:74

for b₁ being TopStruct
for b₂ being Subset of b₁ holds Int b₂ = b₂ \ (Fr b₂)

proof end;

Lemma39: for b₁ being TopStruct
for b₂ being Subset of b₁ holds Fr b₂ = (Cl b₂) \ (Int b₂)

proof end;

Lemma40: for b₁ being TopSpace
for b₂ being Subset of b₁ holds Cl (Fr b₂) = Fr b₂

proof end;

Lemma41: for b₁ being TopSpace
for b₂ being Subset of b₁ holds Int (Fr (Fr b₂)) = {}

proof end;

theorem Th75: :: TOPS_1:75

for b₁ being TopSpace
for b₂ being Subset of b₁ holds Fr (Fr (Fr b₂)) = Fr (Fr b₂)

proof end;

Lemma42: for b₁, b₂, b₃ being set st b₁ c= b₃ & b₂ = b₃ \ b₁ holds
b₁ c= b₃ \ b₂

proof end;

theorem Th76: :: TOPS_1:76

for b₁ being TopSpace
for b₂ being Subset of b₁ holds
( b₂ is open iff Fr b₂ = (Cl b₂) \ b₂ )

proof end;

theorem Th77: :: TOPS_1:77

for b₁ being TopSpace
for b₂ being Subset of b₁ holds
( b₂ is closed iff Fr b₂ = b₂ \ (Int b₂) )

proof end;

definition

let c₁ be TopStruct ;
let c₂ be Subset of c₁;
attr a₂ is dense means :Def3: :: TOPS_1:def 3
Cl a₂ = [#] a₁;

end;

:: deftheorem Def3 defines dense TOPS_1:def 3 :

registration

let c₁ be TopStruct ;
cluster [#] a₁ -> dense ;
coherence

proof end;

end;

theorem Th78: :: TOPS_1:78

canceled;

theorem Th79: :: TOPS_1:79

for b₁ being TopStruct
for b₂, b₃ being Subset of b₁ st b₂ is dense & b₂ c= b₃ holds
b₃ is dense

proof end;

theorem Th80: :: TOPS_1:80

for b₁ being TopSpace
for b₂ being Subset of b₁ holds
( b₂ is dense iff for b₃ being Subset of b₁ st b₃ <> {} & b₃ is open holds
b₂ meets b₃ )

proof end;

theorem Th81: :: TOPS_1:81

for b₁ being TopSpace
for b₂ being Subset of b₁ st b₂ is dense holds
for b₃ being Subset of b₁ st b₃ is open holds
Cl b₃ = Cl (b₃ /\ b₂)

proof end;

theorem Th82: :: TOPS_1:82

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is dense & b₃ is dense & b₃ is open holds
b₂ /\ b₃ is dense

proof end;

definition

let c₁ be TopStruct ;
let c₂ be Subset of c₁;
attr a₂ is boundary means :Def4: :: TOPS_1:def 4
a₂ ` is dense;

end;

:: deftheorem Def4 defines boundary TOPS_1:def 4 :

registration

let c₁ be TopStruct ;
cluster empty -> boundary Element of K10(the carrier of a₁);
coherence

proof end;

end;

registration

let c₁ be TopStruct ;
cluster empty boundary Element of K10(the carrier of a₁);
existence

proof end;

end;

theorem Th83: :: TOPS_1:83

canceled;

theorem Th84: :: TOPS_1:84

for b₁ being TopStruct
for b₂ being Subset of b₁ holds
( b₂ is boundary iff Int b₂ = {} )

proof end;

registration

let c₁ be TopStruct ;
let c₂ be boundary Subset of c₁;
cluster Int a₂ -> empty boundary ;
coherence by Th84;

end;

theorem Th85: :: TOPS_1:85

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is boundary & b₃ is boundary & b₃ is closed holds
b₂ \/ b₃ is boundary

proof end;

theorem Th86: :: TOPS_1:86

for b₁ being TopSpace
for b₂ being Subset of b₁ holds
( b₂ is boundary iff for b₃ being Subset of b₁ st b₃ c= b₂ & b₃ is open holds
b₃ = {} )

proof end;

theorem Th87: :: TOPS_1:87

for b₁ being TopSpace
for b₂ being Subset of b₁ st b₂ is closed holds
( b₂ is boundary iff for b₃ being Subset of b₁ st b₃ <> {} & b₃ is open holds
ex b₄ being Subset of b₁ st
( b₄ c= b₃ & b₄ <> {} & b₄ is open & b₂ misses b₄ ) )

proof end;

theorem Th88: :: TOPS_1:88

for b₁ being TopStruct
for b₂ being Subset of b₁ holds
( b₂ is boundary iff b₂ c= Fr b₂ )

proof end;

definition

let c₁ be TopStruct ;
let c₂ be Subset of c₁;
attr a₂ is nowhere_dense means :Def5: :: TOPS_1:def 5
Cl a₂ is boundary;

end;

:: deftheorem Def5 defines nowhere_dense TOPS_1:def 5 :

registration

let c₁ be TopSpace;
cluster empty -> nowhere_dense Element of K10(the carrier of a₁);
coherence

proof end;

end;

registration

let c₁ be TopSpace;
cluster empty open closed boundary nowhere_dense Element of K10(the carrier of a₁);
existence

proof end;

end;

theorem Th89: :: TOPS_1:89

canceled;

theorem Th90: :: TOPS_1:90

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is nowhere_dense & b₃ is nowhere_dense holds
b₂ \/ b₃ is nowhere_dense

proof end;

theorem Th91: :: TOPS_1:91

for b₁ being TopStruct
for b₂ being Subset of b₁ st b₂ is nowhere_dense holds
b₂ ` is dense

proof end;

registration

let c₁ be TopSpace;
let c₂ be nowhere_dense Subset of c₁;
cluster a₂ ` -> dense ;
coherence by Th91;

end;

theorem Th92: :: TOPS_1:92

for b₁ being TopStruct
for b₂ being Subset of b₁ st b₂ is nowhere_dense holds
b₂ is boundary

proof end;

registration

let c₁ be TopSpace;
cluster nowhere_dense -> boundary Element of K10(the carrier of a₁);
coherence by Th92;

end;

theorem Th93: :: TOPS_1:93

for b₁ being TopStruct
for b₂ being Subset of b₁ st b₂ is boundary & b₂ is closed holds
b₂ is nowhere_dense

proof end;

registration

let c₁ be TopSpace;
cluster closed boundary -> boundary nowhere_dense Element of K10(the carrier of a₁);
coherence by Th93;

end;

theorem Th94: :: TOPS_1:94

for b₁ being TopStruct
for b₂ being Subset of b₁ st b₂ is closed holds
( b₂ is nowhere_dense iff b₂ = Fr b₂ )

proof end;

theorem Th95: :: TOPS_1:95

for b₁ being TopSpace
for b₂ being Subset of b₁ st b₂ is open holds
Fr b₂ is nowhere_dense

proof end;

registration

let c₁ be TopSpace;
let c₂ be open Subset of c₁;
cluster Fr a₂ -> boundary nowhere_dense ;
coherence by Th95;

end;

theorem Th96: :: TOPS_1:96

for b₁ being TopSpace
for b₂ being Subset of b₁ st b₂ is closed holds
Fr b₂ is nowhere_dense

proof end;

registration

let c₁ be TopSpace;
let c₂ be closed Subset of c₁;
cluster Fr a₂ -> boundary nowhere_dense ;
coherence by Th96;

end;

theorem Th97: :: TOPS_1:97

for b₁ being TopSpace
for b₂ being Subset of b₁ st b₂ is open & b₂ is nowhere_dense holds
b₂ = {}

proof end;

registration

let c₁ be TopSpace;
cluster open nowhere_dense -> empty open closed boundary nowhere_dense Element of K10(the carrier of a₁);
coherence by Th97;

end;

definition

let c₁ be TopStruct ;
let c₂ be Subset of c₁;
attr a₂ is condensed means :Def6: :: TOPS_1:def 6
( Int (Cl a₂) c= a₂ & a₂ c= Cl (Int a₂) );
attr a₂ is closed_condensed means :Def7: :: TOPS_1:def 7
a₂ = Cl (Int a₂);
attr a₂ is open_condensed means :Def8: :: TOPS_1:def 8
a₂ = Int (Cl a₂);

end;

:: deftheorem Def6 defines condensed TOPS_1:def 6 :

:: deftheorem Def7 defines closed_condensed TOPS_1:def 7 :

:: deftheorem Def8 defines open_condensed TOPS_1:def 8 :

theorem Th98: :: TOPS_1:98

canceled;

theorem Th99: :: TOPS_1:99

canceled;

theorem Th100: :: TOPS_1:100

canceled;

theorem Th101: :: TOPS_1:101

for b₁ being TopStruct
for b₂ being Subset of b₁ holds
( b₂ is open_condensed iff b₂ ` is closed_condensed )

proof end;

theorem Th102: :: TOPS_1:102

for b₁ being TopStruct
for b₂ being Subset of b₁ st b₂ is closed_condensed holds
Fr (Int b₂) = Fr b₂

proof end;

theorem Th103: :: TOPS_1:103

for b₁ being TopStruct
for b₂ being Subset of b₁ st b₂ is closed_condensed holds
Fr b₂ c= Cl (Int b₂)

proof end;

theorem Th104: :: TOPS_1:104

for b₁ being TopStruct
for b₂ being Subset of b₁ st b₂ is open_condensed holds
( Fr b₂ = Fr (Cl b₂) & Fr (Cl b₂) = (Cl b₂) \ b₂ )

proof end;

theorem Th105: :: TOPS_1:105

for b₁ being TopStruct
for b₂ being Subset of b₁ st b₂ is open & b₂ is closed holds
( b₂ is closed_condensed iff b₂ is open_condensed )

proof end;

theorem Th106: :: TOPS_1:106

for b₁ being TopSpace
for b₂ being TopStruct
for b₃ being Subset of b₁
for b₄ being Subset of b₂ holds
( ( b₄ is closed & b₄ is condensed implies b₄ is closed_condensed ) & ( b₃ is closed_condensed implies ( b₃ is closed & b₃ is condensed ) ) )

proof end;

theorem Th107: :: TOPS_1:107

for b₁ being TopSpace
for b₂ being TopStruct
for b₃ being Subset of b₁
for b₄ being Subset of b₂ holds
( ( b₄ is open & b₄ is condensed implies b₄ is open_condensed ) & ( b₃ is open_condensed implies ( b₃ is open & b₃ is condensed ) ) )

proof end;

theorem Th108: :: TOPS_1:108

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is closed_condensed & b₃ is closed_condensed holds
b₂ \/ b₃ is closed_condensed

proof end;

theorem Th109: :: TOPS_1:109

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is open_condensed & b₃ is open_condensed holds
b₂ /\ b₃ is open_condensed

proof end;

theorem Th110: :: TOPS_1:110

for b₁ being TopSpace
for b₂ being Subset of b₁ st b₂ is condensed holds
Int (Fr b₂) = {}

proof end;

theorem Th111: :: TOPS_1:111

for b₁ being TopStruct
for b₂ being Subset of b₁ st b₂ is condensed holds
( Int b₂ is condensed & Cl b₂ is condensed )

proof end;