:: TSEP_1 semantic presentation

Lemma1: for b₁ being set
for b₂, b₃, b₄ being Subset of b₁ st b₂ \ b₃ = {} holds
b₂ misses b₄ \ b₃

proof end;

Lemma2: for b₁ being set
for b₂, b₃, b₄ being Subset of b₁ st b₂ misses b₃ holds
b₂ misses b₃ \ b₄

proof end;

Lemma3: for b₁, b₂, b₃ being set holds (b₁ /\ b₂) \ b₃ = (b₁ \ b₃) /\ (b₂ \ b₃)

proof end;

theorem Th1: :: TSEP_1:1

for b₁ being TopStruct
for b₂ being SubSpace of b₁ holds the carrier of b₂ is Subset of b₁

proof end;

theorem Th2: :: TSEP_1:2

for b₁ being TopStruct holds b₁ is SubSpace of b₁

proof end;

theorem Th3: :: TSEP_1:3

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

proof end;

theorem Th4: :: TSEP_1:4

for b₁ being TopSpace
for b₂, b₃ being SubSpace of b₁ holds
( the carrier of b₂ c= the carrier of b₃ iff b₂ is SubSpace of b₃ )

proof end;

Lemma7: for b₁ being TopStruct
for b₂ being SubSpace of b₁ holds TopStruct(# the carrier of b₂,the topology of b₂ #) is strict SubSpace of b₁

proof end;

theorem Th5: :: TSEP_1:5

for b₁ being TopStruct
for b₂, b₃ being SubSpace of b₁ st the carrier of b₂ = the carrier of b₃ holds
TopStruct(# the carrier of b₂,the topology of b₂ #) = TopStruct(# the carrier of b₃,the topology of b₃ #)

proof end;

theorem Th6: :: TSEP_1:6

for b₁ being TopSpace
for b₂, b₃ being SubSpace of b₁ st b₂ is SubSpace of b₃ & b₃ is SubSpace of b₂ holds
TopStruct(# the carrier of b₂,the topology of b₂ #) = TopStruct(# the carrier of b₃,the topology of b₃ #)

proof end;

theorem Th7: :: TSEP_1:7

for b₁ being TopSpace
for b₂ being SubSpace of b₁
for b₃ being SubSpace of b₂ holds b₃ is SubSpace of b₁

proof end;

theorem Th8: :: TSEP_1:8

for b₁ being TopSpace
for b₂ being SubSpace of b₁
for b₃, b₄ being Subset of b₁
for b₅ being Subset of b₂ st b₃ is closed & b₃ c= the carrier of b₂ & b₄ c= b₃ & b₄ = b₅ holds
( b₅ is closed iff b₄ is closed )

proof end;

theorem Th9: :: TSEP_1:9

for b₁ being TopSpace
for b₂ being SubSpace of b₁
for b₃, b₄ being Subset of b₁
for b₅ being Subset of b₂ st b₃ is open & b₃ c= the carrier of b₂ & b₄ c= b₃ & b₄ = b₅ holds
( b₅ is open iff b₄ is open )

proof end;

theorem Th10: :: TSEP_1:10

for b₁ being non empty TopStruct
for b₂ being non empty Subset of b₁ ex b₃ being non empty strict SubSpace of b₁ st b₂ = the carrier of b₃

proof end;

theorem Th11: :: TSEP_1:11

for b₁ being TopSpace
for b₂ being SubSpace of b₁
for b₃ being Subset of b₁ st b₃ = the carrier of b₂ holds
( b₂ is closed SubSpace of b₁ iff b₃ is closed )

proof end;

theorem Th12: :: TSEP_1:12

for b₁ being TopSpace
for b₂ being closed SubSpace of b₁
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st b₃ = b₄ holds
( b₄ is closed iff b₃ is closed )

proof end;

theorem Th13: :: TSEP_1:13

for b₁ being TopSpace
for b₂ being closed SubSpace of b₁
for b₃ being closed SubSpace of b₂ holds b₃ is closed SubSpace of b₁

proof end;

theorem Th14: :: TSEP_1:14

for b₁ being non empty TopSpace
for b₂ being non empty closed SubSpace of b₁
for b₃ being non empty SubSpace of b₁ st the carrier of b₂ c= the carrier of b₃ holds
b₂ is non empty closed SubSpace of b₃

proof end;

theorem Th15: :: TSEP_1:15

for b₁ being non empty TopSpace
for b₂ being non empty Subset of b₁ st b₂ is closed holds
ex b₃ being non empty strict closed SubSpace of b₁ st b₂ = the carrier of b₃

proof end;

definition

let c₁ be TopStruct ;
let c₂ be SubSpace of c₁;
attr a₂ is open means :Def1: :: TSEP_1:def 1
for b₁ being Subset of a₁ st b₁ = the carrier of a₂ holds
b₁ is open;

end;

:: deftheorem Def1 defines open TSEP_1:def 1 :

Lemma16: for b₁ being TopStruct holds TopStruct(# the carrier of b₁,the topology of b₁ #) is SubSpace of b₁

proof end;

registration

let c₁ be TopSpace;
cluster strict open SubSpace of a₁;
existence

proof end;

end;

registration

let c₁ be non empty TopSpace;
cluster non empty strict open SubSpace of a₁;
existence

proof end;

end;

theorem Th16: :: TSEP_1:16

for b₁ being TopSpace
for b₂ being SubSpace of b₁
for b₃ being Subset of b₁ st b₃ = the carrier of b₂ holds
( b₂ is open SubSpace of b₁ iff b₃ is open )

proof end;

theorem Th17: :: TSEP_1:17

for b₁ being TopSpace
for b₂ being open SubSpace of b₁
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st b₃ = b₄ holds
( b₄ is open iff b₃ is open )

proof end;

theorem Th18: :: TSEP_1:18

for b₁ being TopSpace
for b₂ being open SubSpace of b₁
for b₃ being open SubSpace of b₂ holds b₃ is open SubSpace of b₁

proof end;

theorem Th19: :: TSEP_1:19

for b₁ being non empty TopSpace
for b₂ being open SubSpace of b₁
for b₃ being non empty SubSpace of b₁ st the carrier of b₂ c= the carrier of b₃ holds
b₂ is open SubSpace of b₃

proof end;

theorem Th20: :: TSEP_1:20

for b₁ being non empty TopSpace
for b₂ being non empty Subset of b₁ st b₂ is open holds
ex b₃ being non empty strict open SubSpace of b₁ st b₂ = the carrier of b₃

proof end;

definition

let c₁ be non empty TopStruct ;
let c₂, c₃ be non empty SubSpace of c₁;
func c₂ union c₃ -> non empty strict SubSpace of a₁ means :Def2: :: TSEP_1:def 2
the carrier of a₄ = the carrier of a₂ \/ the carrier of a₃;
existence

proof end;

uniqueness by Th5;
commutativity ;

end;

:: deftheorem Def2 defines union TSEP_1:def 2 :

theorem Th21: :: TSEP_1:21

for b₁ being non empty TopSpace
for b₂, b₃, b₄ being non empty SubSpace of b₁ holds (b₂ union b₃) union b₄ = b₂ union (b₃ union b₄)

proof end;

theorem Th22: :: TSEP_1:22

for b₁ being non empty TopSpace
for b₂, b₃ being non empty SubSpace of b₁ holds b₂ is SubSpace of b₂ union b₃

proof end;

theorem Th23: :: TSEP_1:23

for b₁ being non empty TopSpace
for b₂, b₃ being non empty SubSpace of b₁ holds
( b₂ is SubSpace of b₃ iff b₂ union b₃ = TopStruct(# the carrier of b₃,the topology of b₃ #) )

proof end;

theorem Th24: :: TSEP_1:24

for b₁ being non empty TopSpace
for b₂, b₃ being non empty closed SubSpace of b₁ holds b₂ union b₃ is closed SubSpace of b₁

proof end;

theorem Th25: :: TSEP_1:25

for b₁ being non empty TopSpace
for b₂, b₃ being non empty open SubSpace of b₁ holds b₂ union b₃ is open SubSpace of b₁

proof end;

definition

let c₁ be TopStruct ;
let c₂, c₃ be SubSpace of c₁;
pred c₂ misses c₃ means :Def3: :: TSEP_1:def 3
the carrier of a₂ misses the carrier of a₃;
correctness ;
symmetry ;

end;

:: deftheorem Def3 defines misses TSEP_1:def 3 :

notation

let c₁ be TopStruct ;
let c₂, c₃ be SubSpace of c₁;
antonym c₂ meets c₃ for c₂ misses c₃;

end;

definition

let c₁ be non empty TopStruct ;
let c₂, c₃ be non empty SubSpace of c₁;
assume E22: c₂ meets c₃ ;
canceled;
func c₂ meet c₃ -> non empty strict SubSpace of a₁ means :Def5: :: TSEP_1:def 5
the carrier of a₄ = the carrier of a₂ /\ the carrier of a₃;
existence

proof end;

uniqueness by Th5;

end;

:: deftheorem Def4 TSEP_1:def 4 :

:: deftheorem Def5 defines meet TSEP_1:def 5 :

theorem Th26: :: TSEP_1:26

canceled;

theorem Th27: :: TSEP_1:27

canceled;

theorem Th28: :: TSEP_1:28

canceled;

theorem Th29: :: TSEP_1:29

for b₁ being non empty TopSpace
for b₂, b₃, b₄ being non empty SubSpace of b₁ holds
( ( b₂ meets b₃ implies b₂ meet b₃ = b₃ meet b₂ ) & ( ( ( b₂ meets b₃ & b₂ meet b₃ meets b₄ ) or ( b₃ meets b₄ & b₂ meets b₃ meet b₄ ) ) implies (b₂ meet b₃) meet b₄ = b₂ meet (b₃ meet b₄) ) )

proof end;

theorem Th30: :: TSEP_1:30

for b₁ being non empty TopSpace
for b₂, b₃ being non empty SubSpace of b₁ st b₂ meets b₃ holds
( b₂ meet b₃ is SubSpace of b₂ & b₂ meet b₃ is SubSpace of b₃ )

proof end;

theorem Th31: :: TSEP_1:31

for b₁ being non empty TopSpace
for b₂, b₃ being non empty SubSpace of b₁ st b₂ meets b₃ holds
( ( b₂ is SubSpace of b₃ implies b₂ meet b₃ = TopStruct(# the carrier of b₂,the topology of b₂ #) ) & ( b₂ meet b₃ = TopStruct(# the carrier of b₂,the topology of b₂ #) implies b₂ is SubSpace of b₃ ) & ( b₃ is SubSpace of b₂ implies b₂ meet b₃ = TopStruct(# the carrier of b₃,the topology of b₃ #) ) & ( b₂ meet b₃ = TopStruct(# the carrier of b₃,the topology of b₃ #) implies b₃ is SubSpace of b₂ ) )

proof end;

theorem Th32: :: TSEP_1:32

for b₁ being non empty TopSpace
for b₂, b₃ being non empty closed SubSpace of b₁ st b₂ meets b₃ holds
b₂ meet b₃ is closed SubSpace of b₁

proof end;

theorem Th33: :: TSEP_1:33

for b₁ being non empty TopSpace
for b₂, b₃ being non empty open SubSpace of b₁ st b₂ meets b₃ holds
b₂ meet b₃ is open SubSpace of b₁

proof end;

theorem Th34: :: TSEP_1:34

for b₁ being non empty TopSpace
for b₂, b₃ being non empty SubSpace of b₁ st b₂ meets b₃ holds
b₂ meet b₃ is SubSpace of b₂ union b₃

proof end;

theorem Th35: :: TSEP_1:35

for b₁ being non empty TopSpace
for b₂, b₃, b₄ being non empty SubSpace of b₁ st b₂ meets b₄ & b₄ meets b₃ holds
( (b₂ union b₃) meet b₄ = (b₂ meet b₄) union (b₃ meet b₄) & b₄ meet (b₂ union b₃) = (b₄ meet b₂) union (b₄ meet b₃) )

proof end;

theorem Th36: :: TSEP_1:36

for b₁ being non empty TopSpace
for b₂, b₃, b₄ being non empty SubSpace of b₁ st b₂ meets b₃ holds
( (b₂ meet b₃) union b₄ = (b₂ union b₄) meet (b₃ union b₄) & b₄ union (b₂ meet b₃) = (b₄ union b₂) meet (b₄ union b₃) )

proof end;

notation

let c₁ be TopStruct ;
let c₂, c₃ be Subset of c₁;
antonym c₂,c₃ are_not_separated for c₂,c₃ are_separated ;

end;

theorem Th37: :: TSEP_1:37

canceled;

theorem Th38: :: TSEP_1:38

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is closed & b₃ is closed holds
( b₂ misses b₃ iff b₂,b₃ are_separated )

proof end;

theorem Th39: :: TSEP_1:39

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

proof end;

theorem Th40: :: TSEP_1:40

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ st b₂ misses b₃ & b₂ is open holds
b₂ misses Cl b₃

proof end;

theorem Th41: :: TSEP_1:41

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is open & b₃ is open holds
( b₂ misses b₃ iff b₂,b₃ are_separated )

proof end;

theorem Th42: :: TSEP_1:42

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

proof end;

theorem Th43: :: TSEP_1:43

for b₁ being TopSpace
for b₂, b₃, b₄ being Subset of b₁ st b₂,b₃ are_separated holds
b₂ /\ b₄,b₃ /\ b₄ are_separated

proof end;

theorem Th44: :: TSEP_1:44

for b₁ being TopSpace
for b₂, b₃, b₄ being Subset of b₁ st ( b₂,b₄ are_separated or b₃,b₄ are_separated ) holds
b₂ /\ b₃,b₄ are_separated

proof end;

theorem Th45: :: TSEP_1:45

for b₁ being TopSpace
for b₂, b₃, b₄ being Subset of b₁ holds
( ( b₂,b₄ are_separated & b₃,b₄ are_separated ) iff b₂ \/ b₃,b₄ are_separated )

proof end;

theorem Th46: :: TSEP_1:46

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ holds
( b₂,b₃ are_separated iff ex b₄, b₅ being Subset of b₁ st
( b₂ c= b₄ & b₃ c= b₅ & b₄ misses b₃ & b₅ misses b₂ & b₄ is closed & b₅ is closed ) )

proof end;

theorem Th47: :: TSEP_1:47

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ holds
( b₂,b₃ are_separated iff ex b₄, b₅ being Subset of b₁ st
( b₂ c= b₄ & b₃ c= b₅ & b₄ /\ b₅ misses b₂ \/ b₃ & b₄ is closed & b₅ is closed ) )

proof end;

theorem Th48: :: TSEP_1:48

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ holds
( b₂,b₃ are_separated iff ex b₄, b₅ being Subset of b₁ st
( b₂ c= b₄ & b₃ c= b₅ & b₄ misses b₃ & b₅ misses b₂ & b₄ is open & b₅ is open ) )

proof end;

theorem Th49: :: TSEP_1:49

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ holds
( b₂,b₃ are_separated iff ex b₄, b₅ being Subset of b₁ st
( b₂ c= b₄ & b₃ c= b₅ & b₄ /\ b₅ misses b₂ \/ b₃ & b₄ is open & b₅ is open ) )

proof end;

definition

let c₁ be TopStruct ;
let c₂, c₃ be Subset of c₁;
canceled;
pred c₂,c₃ are_weakly_separated means :Def7: :: TSEP_1:def 7
a₂ \ a₃,a₃ \ a₂ are_separated ;
symmetry ;

end;

:: deftheorem Def6 TSEP_1:def 6 :

:: deftheorem Def7 defines are_weakly_separated TSEP_1:def 7 :

notation

let c₁ be TopStruct ;
let c₂, c₃ be Subset of c₁;
antonym c₂,c₃ are_not_weakly_separated for c₂,c₃ are_weakly_separated ;

end;

theorem Th50: :: TSEP_1:50

canceled;

theorem Th51: :: TSEP_1:51

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ holds
( ( b₂ misses b₃ & b₂,b₃ are_weakly_separated ) iff b₂,b₃ are_separated )

proof end;

theorem Th52: :: TSEP_1:52

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ st b₂ c= b₃ holds
b₂,b₃ are_weakly_separated

proof end;

theorem Th53: :: TSEP_1:53

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

proof end;

theorem Th54: :: TSEP_1:54

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

proof end;

theorem Th55: :: TSEP_1:55

for b₁ being TopSpace
for b₂, b₃, b₄ being Subset of b₁ st b₂,b₃ are_weakly_separated holds
b₂ \/ b₄,b₃ \/ b₄ are_weakly_separated

proof end;

theorem Th56: :: TSEP_1:56

for b₁ being TopSpace
for b₂, b₃, b₄, b₅ being Subset of b₁ st b₄ c= b₂ & b₅ c= b₃ & b₃,b₂ are_weakly_separated holds
b₃ \/ b₄,b₂ \/ b₅ are_weakly_separated

proof end;

theorem Th57: :: TSEP_1:57

for b₁ being TopSpace
for b₂, b₃, b₄ being Subset of b₁ st b₂,b₄ are_weakly_separated & b₃,b₄ are_weakly_separated holds
b₂ /\ b₃,b₄ are_weakly_separated

proof end;

theorem Th58: :: TSEP_1:58

for b₁ being TopSpace
for b₂, b₃, b₄ being Subset of b₁ st b₂,b₄ are_weakly_separated & b₃,b₄ are_weakly_separated holds
b₂ \/ b₃,b₄ are_weakly_separated

proof end;

theorem Th59: :: TSEP_1:59

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ holds
( b₂,b₃ are_weakly_separated iff ex b₄, b₅, b₆ being Subset of b₁ st
( b₄ /\ (b₂ \/ b₃) c= b₂ & b₅ /\ (b₂ \/ b₃) c= b₃ & b₆ /\ (b₂ \/ b₃) c= b₂ /\ b₃ & the carrier of b₁ = (b₄ \/ b₅) \/ b₆ & b₄ is closed & b₅ is closed & b₆ is open ) )

proof end;

theorem Th60: :: TSEP_1:60

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂,b₃ are_weakly_separated & not b₂ c= b₃ & not b₃ c= b₂ holds
ex b₄, b₅ being non empty Subset of b₁ st
( b₄ is closed & b₅ is closed & b₄ /\ (b₂ \/ b₃) c= b₂ & b₅ /\ (b₂ \/ b₃) c= b₃ & ( b₂ \/ b₃ c= b₄ \/ b₅ or ex b₆ being non empty Subset of b₁ st
( b₆ is open & b₆ /\ (b₂ \/ b₃) c= b₂ /\ b₃ & the carrier of b₁ = (b₄ \/ b₅) \/ b₆ ) ) )

proof end;

theorem Th61: :: TSEP_1:61

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂ \/ b₃ = the carrier of b₁ holds
( b₂,b₃ are_weakly_separated iff ex b₄, b₅, b₆ being Subset of b₁ st
( b₂ \/ b₃ = (b₄ \/ b₅) \/ b₆ & b₄ c= b₂ & b₅ c= b₃ & b₆ c= b₂ /\ b₃ & b₄ is closed & b₅ is closed & b₆ is open ) )

proof end;

theorem Th62: :: TSEP_1:62

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂ \/ b₃ = the carrier of b₁ & b₂,b₃ are_weakly_separated & not b₂ c= b₃ & not b₃ c= b₂ holds
ex b₄, b₅ being non empty Subset of b₁ st
( b₄ is closed & b₅ is closed & b₄ c= b₂ & b₅ c= b₃ & ( b₂ \/ b₃ = b₄ \/ b₅ or ex b₆ being non empty Subset of b₁ st
( b₂ \/ b₃ = (b₄ \/ b₅) \/ b₆ & b₆ c= b₂ /\ b₃ & b₆ is open ) ) )

proof end;

theorem Th63: :: TSEP_1:63

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ holds
( b₂,b₃ are_weakly_separated iff ex b₄, b₅, b₆ being Subset of b₁ st
( b₄ /\ (b₂ \/ b₃) c= b₂ & b₅ /\ (b₂ \/ b₃) c= b₃ & b₆ /\ (b₂ \/ b₃) c= b₂ /\ b₃ & the carrier of b₁ = (b₄ \/ b₅) \/ b₆ & b₄ is open & b₅ is open & b₆ is closed ) )

proof end;

theorem Th64: :: TSEP_1:64

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂,b₃ are_weakly_separated & not b₂ c= b₃ & not b₃ c= b₂ holds
ex b₄, b₅ being non empty Subset of b₁ st
( b₄ is open & b₅ is open & b₄ /\ (b₂ \/ b₃) c= b₂ & b₅ /\ (b₂ \/ b₃) c= b₃ & ( b₂ \/ b₃ c= b₄ \/ b₅ or ex b₆ being non empty Subset of b₁ st
( b₆ is closed & b₆ /\ (b₂ \/ b₃) c= b₂ /\ b₃ & the carrier of b₁ = (b₄ \/ b₅) \/ b₆ ) ) )

proof end;

theorem Th65: :: TSEP_1:65

proof end;

theorem Th66: :: TSEP_1:66

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂ \/ b₃ = the carrier of b₁ & b₂,b₃ are_weakly_separated & not b₂ c= b₃ & not b₃ c= b₂ holds
ex b₄, b₅ being non empty Subset of b₁ st
( b₄ is open & b₅ is open & b₄ c= b₂ & b₅ c= b₃ & ( b₂ \/ b₃ = b₄ \/ b₅ or ex b₆ being non empty Subset of b₁ st
( b₂ \/ b₃ = (b₄ \/ b₅) \/ b₆ & b₆ c= b₂ /\ b₃ & b₆ is closed ) ) )

proof end;

theorem Th67: :: TSEP_1:67

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ holds
( b₂,b₃ are_separated iff ex b₄, b₅ being Subset of b₁ st
( b₄,b₅ are_weakly_separated & b₂ c= b₄ & b₃ c= b₅ & b₄ /\ b₅ misses b₂ \/ b₃ ) )

proof end;

definition

let c₁ be TopStruct ;
let c₂, c₃ be SubSpace of c₁;
pred c₂,c₃ are_separated means :Def8: :: TSEP_1:def 8
for b₁, b₂ being Subset of a₁ st b₁ = the carrier of a₂ & b₂ = the carrier of a₃ holds
b₁,b₂ are_separated ;
symmetry ;

end;

:: deftheorem Def8 defines are_separated TSEP_1:def 8 :

notation

let c₁ be TopStruct ;
let c₂, c₃ be SubSpace of c₁;
antonym c₂,c₃ are_not_separated for c₂,c₃ are_separated ;

end;

theorem Th68: :: TSEP_1:68

for b₁ being non empty TopSpace
for b₂, b₃ being non empty SubSpace of b₁ st b₂,b₃ are_separated holds
b₂ misses b₃

proof end;

theorem Th69: :: TSEP_1:69

canceled;

theorem Th70: :: TSEP_1:70

for b₁ being non empty TopSpace
for b₂, b₃ being non empty closed SubSpace of b₁ holds
( b₂ misses b₃ iff b₂,b₃ are_separated )

proof end;

theorem Th71: :: TSEP_1:71

for b₁ being non empty TopSpace
for b₂, b₃ being non empty SubSpace of b₁ st b₁ = b₂ union b₃ & b₂,b₃ are_separated holds
b₂ is closed SubSpace of b₁

proof end;

theorem Th72: :: TSEP_1:72

for b₁ being non empty TopSpace
for b₂, b₃ being non empty SubSpace of b₁ st b₂ union b₃ is closed SubSpace of b₁ & b₂,b₃ are_separated holds
b₂ is closed SubSpace of b₁

proof end;

theorem Th73: :: TSEP_1:73

for b₁ being non empty TopSpace
for b₂, b₃ being non empty open SubSpace of b₁ holds
( b₂ misses b₃ iff b₂,b₃ are_separated )

proof end;

theorem Th74: :: TSEP_1:74

for b₁ being non empty TopSpace
for b₂, b₃ being non empty SubSpace of b₁ st b₁ = b₂ union b₃ & b₂,b₃ are_separated holds
b₂ is open SubSpace of b₁

proof end;

theorem Th75: :: TSEP_1:75

for b₁ being non empty TopSpace
for b₂, b₃ being non empty SubSpace of b₁ st b₂ union b₃ is open SubSpace of b₁ & b₂,b₃ are_separated holds
b₂ is open SubSpace of b₁

proof end;

theorem Th76: :: TSEP_1:76

for b₁ being non empty TopSpace
for b₂, b₃, b₄ being non empty SubSpace of b₁ st b₃ meets b₂ & b₄ meets b₂ & b₃,b₄ are_separated holds
( b₃ meet b₂,b₄ meet b₂ are_separated & b₂ meet b₃,b₂ meet b₄ are_separated )

proof end;

theorem Th77: :: TSEP_1:77

for b₁ being non empty TopSpace
for b₂, b₃ being non empty SubSpace of b₁
for b₄, b₅ being SubSpace of b₁ st b₄ is SubSpace of b₂ & b₅ is SubSpace of b₃ & b₂,b₃ are_separated holds
b₄,b₅ are_separated

proof end;

theorem Th78: :: TSEP_1:78

for b₁ being non empty TopSpace
for b₂, b₃, b₄ being non empty SubSpace of b₁ st b₂ meets b₃ & b₂,b₄ are_separated holds
b₂ meet b₃,b₄ are_separated

proof end;

theorem Th79: :: TSEP_1:79

for b₁ being non empty TopSpace
for b₂, b₃, b₄ being non empty SubSpace of b₁ holds
( ( b₂,b₄ are_separated & b₃,b₄ are_separated ) iff b₂ union b₃,b₄ are_separated )

proof end;

theorem Th80: :: TSEP_1:80

for b₁ being non empty TopSpace
for b₂, b₃ being non empty SubSpace of b₁ holds
( b₂,b₃ are_separated iff ex b₄, b₅ being non empty closed SubSpace of b₁ st
( b₂ is SubSpace of b₄ & b₃ is SubSpace of b₅ & b₄ misses b₃ & b₅ misses b₂ ) )

proof end;

theorem Th81: :: TSEP_1:81

proof end;

theorem Th82: :: TSEP_1:82

for b₁ being non empty TopSpace
for b₂, b₃ being non empty SubSpace of b₁ holds
( b₂,b₃ are_separated iff ex b₄, b₅ being non empty open SubSpace of b₁ st
( b₂ is SubSpace of b₄ & b₃ is SubSpace of b₅ & b₄ misses b₃ & b₅ misses b₂ ) )

proof end;

theorem Th83: :: TSEP_1:83

proof end;

definition

let c₁ be TopStruct ;
let c₂, c₃ be SubSpace of c₁;
pred c₂,c₃ are_weakly_separated means :Def9: :: TSEP_1:def 9
for b₁, b₂ being Subset of a₁ st b₁ = the carrier of a₂ & b₂ = the carrier of a₃ holds
b₁,b₂ are_weakly_separated ;
symmetry ;

end;

:: deftheorem Def9 defines are_weakly_separated TSEP_1:def 9 :

notation

let c₁ be TopStruct ;
let c₂, c₃ be SubSpace of c₁;
antonym c₂,c₃ are_not_weakly_separated for c₂,c₃ are_weakly_separated ;

end;

theorem Th84: :: TSEP_1:84

canceled;

theorem Th85: :: TSEP_1:85

for b₁ being non empty TopSpace
for b₂, b₃ being non empty SubSpace of b₁ holds
( ( b₂ misses b₃ & b₂,b₃ are_weakly_separated ) iff b₂,b₃ are_separated )

proof end;

theorem Th86: :: TSEP_1:86

for b₁ being non empty TopSpace
for b₂, b₃ being non empty SubSpace of b₁ st b₂ is SubSpace of b₃ holds
b₂,b₃ are_weakly_separated

proof end;

theorem Th87: :: TSEP_1:87

for b₁ being non empty TopSpace
for b₂, b₃ being closed SubSpace of b₁ holds b₂,b₃ are_weakly_separated

proof end;

theorem Th88: :: TSEP_1:88

for b₁ being non empty TopSpace
for b₂, b₃ being open SubSpace of b₁ holds b₂,b₃ are_weakly_separated

proof end;

theorem Th89: :: TSEP_1:89

for b₁ being non empty TopSpace
for b₂, b₃, b₄ being non empty SubSpace of b₁ st b₂,b₃ are_weakly_separated holds
b₂ union b₄,b₃ union b₄ are_weakly_separated

proof end;

theorem Th90: :: TSEP_1:90

for b₁ being non empty TopSpace
for b₂, b₃, b₄, b₅ being non empty SubSpace of b₁ st b₄ is SubSpace of b₂ & b₅ is SubSpace of b₃ & b₃,b₂ are_weakly_separated holds
( b₃ union b₄,b₂ union b₅ are_weakly_separated & b₄ union b₃,b₅ union b₂ are_weakly_separated )

proof end;

theorem Th91: :: TSEP_1:91

for b₁ being non empty TopSpace
for b₂, b₃, b₄ being non empty SubSpace of b₁ st b₃ meets b₄ holds
( ( b₃,b₂ are_weakly_separated & b₄,b₂ are_weakly_separated implies b₃ meet b₄,b₂ are_weakly_separated ) & ( b₂,b₃ are_weakly_separated & b₂,b₄ are_weakly_separated implies b₂,b₃ meet b₄ are_weakly_separated ) )

proof end;

theorem Th92: :: TSEP_1:92

for b₁ being non empty TopSpace
for b₂, b₃, b₄ being non empty SubSpace of b₁ holds
( ( b₂,b₄ are_weakly_separated & b₃,b₄ are_weakly_separated implies b₂ union b₃,b₄ are_weakly_separated ) & ( b₄,b₂ are_weakly_separated & b₄,b₃ are_weakly_separated implies b₄,b₂ union b₃ are_weakly_separated ) )

proof end;

theorem Th93: :: TSEP_1:93

for b₁ being non empty TopSpace
for b₂, b₃ being non empty SubSpace of b₁ st b₂ meets b₃ holds
( b₂,b₃ are_weakly_separated iff ( b₂ is SubSpace of b₃ or b₃ is SubSpace of b₂ or ex b₄, b₅ being non empty closed SubSpace of b₁ st
( b₄ meet (b₂ union b₃) is SubSpace of b₂ & b₅ meet (b₂ union b₃) is SubSpace of b₃ & ( b₂ union b₃ is SubSpace of b₄ union b₅ or ex b₆ being non empty open SubSpace of b₁ st
( TopStruct(# the carrier of b₁,the topology of b₁ #) = (b₄ union b₅) union b₆ & b₆ meet (b₂ union b₃) is SubSpace of b₂ meet b₃ ) ) ) ) )

proof end;

theorem Th94: :: TSEP_1:94

for b₁ being non empty TopSpace
for b₂, b₃ being non empty SubSpace of b₁ st b₁ = b₂ union b₃ & b₂ meets b₃ holds
( b₂,b₃ are_weakly_separated iff ( b₂ is SubSpace of b₃ or b₃ is SubSpace of b₂ or ex b₄, b₅ being non empty closed SubSpace of b₁ st
( b₄ is SubSpace of b₂ & b₅ is SubSpace of b₃ & ( b₁ = b₄ union b₅ or ex b₆ being non empty open SubSpace of b₁ st
( b₁ = (b₄ union b₅) union b₆ & b₆ is SubSpace of b₂ meet b₃ ) ) ) ) )

proof end;

theorem Th95: :: TSEP_1:95

for b₁ being non empty TopSpace
for b₂, b₃ being non empty SubSpace of b₁ st b₁ = b₂ union b₃ & b₂ misses b₃ holds
( b₂,b₃ are_weakly_separated iff ( b₂ is closed SubSpace of b₁ & b₃ is closed SubSpace of b₁ ) )

proof end;

theorem Th96: :: TSEP_1:96

for b₁ being non empty TopSpace
for b₂, b₃ being non empty SubSpace of b₁ st b₂ meets b₃ holds
( b₂,b₃ are_weakly_separated iff ( b₂ is SubSpace of b₃ or b₃ is SubSpace of b₂ or ex b₄, b₅ being non empty open SubSpace of b₁ st
( b₄ meet (b₂ union b₃) is SubSpace of b₂ & b₅ meet (b₂ union b₃) is SubSpace of b₃ & ( b₂ union b₃ is SubSpace of b₄ union b₅ or ex b₆ being non empty closed SubSpace of b₁ st
( TopStruct(# the carrier of b₁,the topology of b₁ #) = (b₄ union b₅) union b₆ & b₆ meet (b₂ union b₃) is SubSpace of b₂ meet b₃ ) ) ) ) )

proof end;

theorem Th97: :: TSEP_1:97

for b₁ being non empty TopSpace
for b₂, b₃ being non empty SubSpace of b₁ st b₁ = b₂ union b₃ & b₂ meets b₃ holds
( b₂,b₃ are_weakly_separated iff ( b₂ is SubSpace of b₃ or b₃ is SubSpace of b₂ or ex b₄, b₅ being non empty open SubSpace of b₁ st
( b₄ is SubSpace of b₂ & b₅ is SubSpace of b₃ & ( b₁ = b₄ union b₅ or ex b₆ being non empty closed SubSpace of b₁ st
( b₁ = (b₄ union b₅) union b₆ & b₆ is SubSpace of b₂ meet b₃ ) ) ) ) )

proof end;

theorem Th98: :: TSEP_1:98

for b₁ being non empty TopSpace
for b₂, b₃ being non empty SubSpace of b₁ st b₁ = b₂ union b₃ & b₂ misses b₃ holds
( b₂,b₃ are_weakly_separated iff ( b₂ is open SubSpace of b₁ & b₃ is open SubSpace of b₁ ) )

proof end;

theorem Th99: :: TSEP_1:99

for b₁ being non empty TopSpace
for b₂, b₃ being non empty SubSpace of b₁ holds
( b₂,b₃ are_separated iff ex b₄, b₅ being non empty SubSpace of b₁ st
( b₄,b₅ are_weakly_separated & b₂ is SubSpace of b₄ & b₃ is SubSpace of b₅ & ( b₄ misses b₅ or b₄ meet b₅ misses b₂ union b₃ ) ) )

proof end;