:: Separated and Weakly Separated Subspaces of Topological Spaces
:: by Zbigniew Karno
::
:: Received January 8, 1992
:: Copyright (c) 1992 Association of Mizar Users


begin

Lm1: for A being set
for B, C, D being Subset of A st B \ C = {} holds
B misses D \ C
proof end;

Lm2: for A, B, C being set holds (A /\ B) \ C = (A \ C) /\ (B \ C)
proof end;

theorem Th1: :: TSEP_1:1
for X being TopStruct
for X0 being SubSpace of X holds the carrier of X0 is Subset of X
proof end;

theorem Th2: :: TSEP_1:2
for X being TopStruct holds X is SubSpace of X
proof end;

theorem :: TSEP_1:3
for X being strict TopStruct holds X | ([#] X) = X
proof end;

theorem Th4: :: TSEP_1:4
for X being TopSpace
for X1, X2 being SubSpace of X holds
( the carrier of X1 c= the carrier of X2 iff X1 is SubSpace of X2 )
proof end;

Lm3: for X being TopStruct
for X0 being SubSpace of X holds TopStruct(# the carrier of X0, the topology of X0 #) is strict SubSpace of X
proof end;

theorem Th5: :: TSEP_1:5
for X being TopStruct
for X1, X2 being SubSpace of X st the carrier of X1 = the carrier of X2 holds
TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)
proof end;

theorem :: TSEP_1:6
for X being TopSpace
for X1, X2 being SubSpace of X st X1 is SubSpace of X2 & X2 is SubSpace of X1 holds
TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)
proof end;

theorem Th7: :: TSEP_1:7
for X being TopSpace
for X1 being SubSpace of X
for X2 being SubSpace of X1 holds X2 is SubSpace of X
proof end;

theorem Th8: :: TSEP_1:8
for X being TopSpace
for X0 being SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C is closed & C c= the carrier of X0 & A c= C & A = B holds
( B is closed iff A is closed )
proof end;

theorem Th9: :: TSEP_1:9
for X being TopSpace
for X0 being SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B holds
( B is open iff A is open )
proof end;

theorem Th10: :: TSEP_1:10
for X being non empty TopStruct
for A0 being non empty Subset of X ex X0 being non empty strict SubSpace of X st A0 = the carrier of X0
proof end;

theorem Th11: :: TSEP_1:11
for X being TopSpace
for X0 being SubSpace of X
for A being Subset of X st A = the carrier of X0 holds
( X0 is closed SubSpace of X iff A is closed )
proof end;

theorem :: TSEP_1:12
for X being TopSpace
for X0 being closed SubSpace of X
for A being Subset of X
for B being Subset of X0 st A = B holds
( B is closed iff A is closed )
proof end;

theorem :: TSEP_1:13
for X being TopSpace
for X1 being closed SubSpace of X
for X2 being closed SubSpace of X1 holds X2 is closed SubSpace of X
proof end;

theorem :: TSEP_1:14
for X being non empty TopSpace
for X1 being non empty closed SubSpace of X
for X2 being non empty SubSpace of X st the carrier of X1 c= the carrier of X2 holds
X1 is non empty closed SubSpace of X2
proof end;

theorem Th15: :: TSEP_1:15
for X being non empty TopSpace
for A0 being non empty Subset of X st A0 is closed holds
ex X0 being non empty strict closed SubSpace of X st A0 = the carrier of X0
proof end;

definition
let X be TopStruct ;
let IT be SubSpace of X;
attr IT is open means :Def1: :: TSEP_1:def 1
 for A being Subset of X st A = the carrier of IT holds
A is open ;
end;

:: deftheorem Def1 defines open TSEP_1:def 1 :
for X being TopStruct
for IT being SubSpace of X holds
( IT is open iff for A being Subset of X st A = the carrier of IT holds
A is open );

Lm4: for T being TopStruct holds TopStruct(# the carrier of T, the topology of T #) is SubSpace of T
proof end;

registration
let X be TopSpace;
cluster strict TopSpace-like open SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is strict & b1 is open )
proof end;
end;

registration
let X be non empty TopSpace;
cluster non empty strict TopSpace-like open SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is strict & b1 is open & not b1 is empty )
proof end;
end;

theorem Th16: :: TSEP_1:16
for X being TopSpace
for X0 being SubSpace of X
for A being Subset of X st A = the carrier of X0 holds
( X0 is open SubSpace of X iff A is open )
proof end;

theorem :: TSEP_1:17
for X being TopSpace
for X0 being open SubSpace of X
for A being Subset of X
for B being Subset of X0 st A = B holds
( B is open iff A is open )
proof end;

theorem :: TSEP_1:18
for X being TopSpace
for X1 being open SubSpace of X
for X2 being open SubSpace of X1 holds X2 is open SubSpace of X
proof end;

theorem :: TSEP_1:19
for X being non empty TopSpace
for X1 being open SubSpace of X
for X2 being non empty SubSpace of X st the carrier of X1 c= the carrier of X2 holds
X1 is open SubSpace of X2
proof end;

theorem Th20: :: TSEP_1:20
for X being non empty TopSpace
for A0 being non empty Subset of X st A0 is open holds
ex X0 being non empty strict open SubSpace of X st A0 = the carrier of X0
proof end;

begin

definition
let X be non empty TopStruct ;
let X1, X2 be non empty SubSpace of X;
func X1 union X2 -> non empty strict SubSpace of X means :Def2: :: TSEP_1:def 2
 the carrier of it = the carrier of X1 \/ the carrier of X2;
existence
ex b1 being non empty strict SubSpace of X st the carrier of b1 = the carrier of X1 \/ the carrier of X2
proof end;
uniqueness
for b1, b2 being non empty strict SubSpace of X st the carrier of b1 = the carrier of X1 \/ the carrier of X2 & the carrier of b2 = the carrier of X1 \/ the carrier of X2 holds
b1 = b2 by Th5;
commutativity
for b1 being non empty strict SubSpace of X
for X1, X2 being non empty SubSpace of X st the carrier of b1 = the carrier of X1 \/ the carrier of X2 holds
the carrier of b1 = the carrier of X2 \/ the carrier of X1 ;
end;

:: deftheorem Def2 defines union TSEP_1:def 2 :
for X being non empty TopStruct
for X1, X2 being non empty SubSpace of X
for b4 being non empty strict SubSpace of X holds
( b4 = X1 union X2 iff the carrier of b4 = the carrier of X1 \/ the carrier of X2 );

theorem :: TSEP_1:21
for X being non empty TopSpace
for X1, X2, X3 being non empty SubSpace of X holds (X1 union X2) union X3 = X1 union (X2 union X3)
proof end;

theorem Th22: :: TSEP_1:22
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X holds X1 is SubSpace of X1 union X2
proof end;

theorem :: TSEP_1:23
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X holds
( X1 is SubSpace of X2 iff X1 union X2 = TopStruct(# the carrier of X2, the topology of X2 #) )
proof end;

theorem :: TSEP_1:24
for X being non empty TopSpace
for X1, X2 being non empty closed SubSpace of X holds X1 union X2 is closed SubSpace of X
proof end;

theorem :: TSEP_1:25
for X being non empty TopSpace
for X1, X2 being non empty open SubSpace of X holds X1 union X2 is open SubSpace of X
proof end;

definition
let X1, X2 be 1-sorted ;
pred X1 misses X2 means :Def3: :: TSEP_1:def 3
 the carrier of X1 misses the carrier of X2;
correctness
;
symmetry
for X1, X2 being 1-sorted st the carrier of X1 misses the carrier of X2 holds
the carrier of X2 misses the carrier of X1 ;
end;

:: deftheorem Def3 defines misses TSEP_1:def 3 :
for X1, X2 being 1-sorted holds
( X1 misses X2 iff the carrier of X1 misses the carrier of X2 );

notation
let X1, X2 be 1-sorted ;
antonym X1 meets X2 for X1 misses X2;
end;

definition
let X be non empty TopStruct ;
let X1, X2 be non empty SubSpace of X;
assume A1: X1 meets X2 ;
canceled;
func X1 meet X2 -> non empty strict SubSpace of X means :Def5: :: TSEP_1:def 5
 the carrier of it = the carrier of X1 /\ the carrier of X2;
existence
ex b1 being non empty strict SubSpace of X st the carrier of b1 = the carrier of X1 /\ the carrier of X2
proof end;
uniqueness
for b1, b2 being non empty strict SubSpace of X st the carrier of b1 = the carrier of X1 /\ the carrier of X2 & the carrier of b2 = the carrier of X1 /\ the carrier of X2 holds
b1 = b2 by Th5;
end;

:: deftheorem TSEP_1:def 4 :
canceled;

:: deftheorem Def5 defines meet TSEP_1:def 5 :
for X being non empty TopStruct
for X1, X2 being non empty SubSpace of X st X1 meets X2 holds
for b4 being non empty strict SubSpace of X holds
( b4 = X1 meet X2 iff the carrier of b4 = the carrier of X1 /\ the carrier of X2 );

theorem :: TSEP_1:26
canceled;

theorem :: TSEP_1:27
canceled;

theorem :: TSEP_1:28
canceled;

theorem Th29: :: TSEP_1:29
for X being non empty TopSpace
for X1, X2, X3 being non empty SubSpace of X holds
( ( X1 meets X2 implies X1 meet X2 = X2 meet X1 ) & ( ( ( X1 meets X2 & X1 meet X2 meets X3 ) or ( X2 meets X3 & X1 meets X2 meet X3 ) ) implies (X1 meet X2) meet X3 = X1 meet (X2 meet X3) ) )
proof end;

theorem Th30: :: TSEP_1:30
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1 meets X2 holds
( X1 meet X2 is SubSpace of X1 & X1 meet X2 is SubSpace of X2 )
proof end;

theorem :: TSEP_1:31
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1 meets X2 holds
( ( X1 is SubSpace of X2 implies X1 meet X2 = TopStruct(# the carrier of X1, the topology of X1 #) ) & ( X1 meet X2 = TopStruct(# the carrier of X1, the topology of X1 #) implies X1 is SubSpace of X2 ) & ( X2 is SubSpace of X1 implies X1 meet X2 = TopStruct(# the carrier of X2, the topology of X2 #) ) & ( X1 meet X2 = TopStruct(# the carrier of X2, the topology of X2 #) implies X2 is SubSpace of X1 ) )
proof end;

theorem :: TSEP_1:32
for X being non empty TopSpace
for X1, X2 being non empty closed SubSpace of X st X1 meets X2 holds
X1 meet X2 is closed SubSpace of X
proof end;

theorem :: TSEP_1:33
for X being non empty TopSpace
for X1, X2 being non empty open SubSpace of X st X1 meets X2 holds
X1 meet X2 is open SubSpace of X
proof end;

theorem :: TSEP_1:34
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1 meets X2 holds
X1 meet X2 is SubSpace of X1 union X2
proof end;

theorem :: TSEP_1:35
for X being non empty TopSpace
for X1, X2, Y being non empty SubSpace of X st X1 meets Y & Y meets X2 holds
( (X1 union X2) meet Y = (X1 meet Y) union (X2 meet Y) & Y meet (X1 union X2) = (Y meet X1) union (Y meet X2) )
proof end;

theorem :: TSEP_1:36
for X being non empty TopSpace
for X1, X2, Y being non empty SubSpace of X st X1 meets X2 holds
( (X1 meet X2) union Y = (X1 union Y) meet (X2 union Y) & Y union (X1 meet X2) = (Y union X1) meet (Y union X2) )
proof end;

begin

notation
let X be TopStruct ;
let A1, A2 be Subset of X;
antonym A1,A2 are_not_separated for A1,A2 are_separated ;
end;

theorem :: TSEP_1:37
canceled;

theorem Th38: :: TSEP_1:38
for X being TopSpace
for A1, A2 being Subset of X st A1 is closed & A2 is closed holds
( A1 misses A2 iff A1,A2 are_separated )
proof end;

theorem Th39: :: TSEP_1:39
for X being TopSpace
for A1, A2 being Subset of X st A1 \/ A2 is closed & A1,A2 are_separated holds
( A1 is closed & A2 is closed )
proof end;

theorem Th40: :: TSEP_1:40
for X being TopSpace
for A1, A2 being Subset of X st A1 misses A2 & A1 is open holds
A1 misses Cl A2
proof end;

theorem Th41: :: TSEP_1:41
for X being TopSpace
for A1, A2 being Subset of X st A1 is open & A2 is open holds
( A1 misses A2 iff A1,A2 are_separated )
proof end;

theorem Th42: :: TSEP_1:42
for X being TopSpace
for A1, A2 being Subset of X st A1 \/ A2 is open & A1,A2 are_separated holds
( A1 is open & A2 is open )
proof end;

theorem Th43: :: TSEP_1:43
for X being TopSpace
for A1, A2, C being Subset of X st A1,A2 are_separated holds
A1 /\ C,A2 /\ C are_separated
proof end;

theorem Th44: :: TSEP_1:44
for X being TopSpace
for A1, A2, B being Subset of X st ( A1,B are_separated or A2,B are_separated ) holds
A1 /\ A2,B are_separated
proof end;

theorem Th45: :: TSEP_1:45
for X being TopSpace
for A1, A2, B being Subset of X holds
( ( A1,B are_separated & A2,B are_separated ) iff A1 \/ A2,B are_separated )
proof end;

theorem Th46: :: TSEP_1:46
for X being TopSpace
for A1, A2 being Subset of X holds
( A1,A2 are_separated iff ex C1, C2 being Subset of X st
( A1 c= C1 & A2 c= C2 & C1 misses A2 & C2 misses A1 & C1 is closed & C2 is closed ) )
proof end;

theorem Th47: :: TSEP_1:47
for X being TopSpace
for A1, A2 being Subset of X holds
( A1,A2 are_separated iff ex C1, C2 being Subset of X st
( A1 c= C1 & A2 c= C2 & C1 /\ C2 misses A1 \/ A2 & C1 is closed & C2 is closed ) )
proof end;

theorem Th48: :: TSEP_1:48
for X being TopSpace
for A1, A2 being Subset of X holds
( A1,A2 are_separated iff ex C1, C2 being Subset of X st
( A1 c= C1 & A2 c= C2 & C1 misses A2 & C2 misses A1 & C1 is open & C2 is open ) )
proof end;

theorem Th49: :: TSEP_1:49
for X being TopSpace
for A1, A2 being Subset of X holds
( A1,A2 are_separated iff ex C1, C2 being Subset of X st
( A1 c= C1 & A2 c= C2 & C1 /\ C2 misses A1 \/ A2 & C1 is open & C2 is open ) )
proof end;

definition
let X be TopStruct ;
let A1, A2 be Subset of X;
canceled;
pred A1,A2 are_weakly_separated means :Def7: :: TSEP_1:def 7
A1 \ A2,A2 \ A1 are_separated ;
symmetry
for A1, A2 being Subset of X st A1 \ A2,A2 \ A1 are_separated holds
A2 \ A1,A1 \ A2 are_separated ;
end;

:: deftheorem TSEP_1:def 6 :
canceled;

:: deftheorem Def7 defines are_weakly_separated TSEP_1:def 7 :
for X being TopStruct
for A1, A2 being Subset of X holds
( A1,A2 are_weakly_separated iff A1 \ A2,A2 \ A1 are_separated );

notation
let X be TopStruct ;
let A1, A2 be Subset of X;
antonym A1,A2 are_not_weakly_separated for A1,A2 are_weakly_separated ;
end;

theorem :: TSEP_1:50
canceled;

theorem Th51: :: TSEP_1:51
for X being TopSpace
for A1, A2 being Subset of X holds
( ( A1 misses A2 & A1,A2 are_weakly_separated ) iff A1,A2 are_separated )
proof end;

theorem Th52: :: TSEP_1:52
for X being TopSpace
for A1, A2 being Subset of X st A1 c= A2 holds
A1,A2 are_weakly_separated
proof end;

theorem Th53: :: TSEP_1:53
for X being TopSpace
for A1, A2 being Subset of X st A1 is closed & A2 is closed holds
A1,A2 are_weakly_separated
proof end;

theorem Th54: :: TSEP_1:54
for X being TopSpace
for A1, A2 being Subset of X st A1 is open & A2 is open holds
A1,A2 are_weakly_separated
proof end;

theorem Th55: :: TSEP_1:55
for X being TopSpace
for A1, A2, C being Subset of X st A1,A2 are_weakly_separated holds
A1 \/ C,A2 \/ C are_weakly_separated
proof end;

theorem Th56: :: TSEP_1:56
for X being TopSpace
for A2, A1, B1, B2 being Subset of X st B1 c= A2 & B2 c= A1 & A1,A2 are_weakly_separated holds
A1 \/ B1,A2 \/ B2 are_weakly_separated
proof end;

theorem Th57: :: TSEP_1:57
for X being TopSpace
for A1, A2, B being Subset of X st A1,B are_weakly_separated & A2,B are_weakly_separated holds
A1 /\ A2,B are_weakly_separated
proof end;

theorem Th58: :: TSEP_1:58
for X being TopSpace
for A1, A2, B being Subset of X st A1,B are_weakly_separated & A2,B are_weakly_separated holds
A1 \/ A2,B are_weakly_separated
proof end;

theorem Th59: :: TSEP_1:59
for X being TopSpace
for A1, A2 being Subset of X holds
( A1,A2 are_weakly_separated iff ex C1, C2, C being Subset of X st
( C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C & C1 is closed & C2 is closed & C is open ) )
proof end;

theorem Th60: :: TSEP_1:60
for X being non empty TopSpace
for A1, A2 being Subset of X st A1,A2 are_weakly_separated & not A1 c= A2 & not A2 c= A1 holds
ex C1, C2 being non empty Subset of X st
( C1 is closed & C2 is closed & C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & ( A1 \/ A2 c= C1 \/ C2 or ex C being non empty Subset of X st
( C is open & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C ) ) )
proof end;

theorem Th61: :: TSEP_1:61
for X being non empty TopSpace
for A1, A2 being Subset of X st A1 \/ A2 = the carrier of X holds
( A1,A2 are_weakly_separated iff ex C1, C2, C being Subset of X st
( A1 \/ A2 = (C1 \/ C2) \/ C & C1 c= A1 & C2 c= A2 & C c= A1 /\ A2 & C1 is closed & C2 is closed & C is open ) )
proof end;

theorem Th62: :: TSEP_1:62
for X being non empty TopSpace
for A1, A2 being Subset of X st A1 \/ A2 = the carrier of X & A1,A2 are_weakly_separated & not A1 c= A2 & not A2 c= A1 holds
ex C1, C2 being non empty Subset of X st
( C1 is closed & C2 is closed & C1 c= A1 & C2 c= A2 & ( A1 \/ A2 = C1 \/ C2 or ex C being non empty Subset of X st
( A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is open ) ) )
proof end;

theorem Th63: :: TSEP_1:63
for X being non empty TopSpace
for A1, A2 being Subset of X holds
( A1,A2 are_weakly_separated iff ex C1, C2, C being Subset of X st
( C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C & C1 is open & C2 is open & C is closed ) )
proof end;

theorem Th64: :: TSEP_1:64
for X being non empty TopSpace
for A1, A2 being Subset of X st A1,A2 are_weakly_separated & not A1 c= A2 & not A2 c= A1 holds
ex C1, C2 being non empty Subset of X st
( C1 is open & C2 is open & C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & ( A1 \/ A2 c= C1 \/ C2 or ex C being non empty Subset of X st
( C is closed & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C ) ) )
proof end;

theorem Th65: :: TSEP_1:65
for X being non empty TopSpace
for A1, A2 being Subset of X st A1 \/ A2 = the carrier of X holds
( A1,A2 are_weakly_separated iff ex C1, C2, C being Subset of X st
( A1 \/ A2 = (C1 \/ C2) \/ C & C1 c= A1 & C2 c= A2 & C c= A1 /\ A2 & C1 is open & C2 is open & C is closed ) )
proof end;

theorem Th66: :: TSEP_1:66
for X being non empty TopSpace
for A1, A2 being Subset of X st A1 \/ A2 = the carrier of X & A1,A2 are_weakly_separated & not A1 c= A2 & not A2 c= A1 holds
ex C1, C2 being non empty Subset of X st
( C1 is open & C2 is open & C1 c= A1 & C2 c= A2 & ( A1 \/ A2 = C1 \/ C2 or ex C being non empty Subset of X st
( A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is closed ) ) )
proof end;

theorem Th67: :: TSEP_1:67
for X being non empty TopSpace
for A1, A2 being Subset of X holds
( A1,A2 are_separated iff ex B1, B2 being Subset of X st
( B1,B2 are_weakly_separated & A1 c= B1 & A2 c= B2 & B1 /\ B2 misses A1 \/ A2 ) )
proof end;

begin

definition
let X be TopStruct ;
let X1, X2 be SubSpace of X;
pred X1,X2 are_separated means :Def8: :: TSEP_1:def 8
 for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds
A1,A2 are_separated ;
symmetry
for X1, X2 being SubSpace of X st ( for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds
A1,A2 are_separated ) holds
for A1, A2 being Subset of X st A1 = the carrier of X2 & A2 = the carrier of X1 holds
A1,A2 are_separated ;
end;

:: deftheorem Def8 defines are_separated TSEP_1:def 8 :
for X being TopStruct
for X1, X2 being SubSpace of X holds
( X1,X2 are_separated iff for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds
A1,A2 are_separated );

notation
let X be TopStruct ;
let X1, X2 be SubSpace of X;
antonym X1,X2 are_not_separated for X1,X2 are_separated ;
end;

theorem :: TSEP_1:68
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1,X2 are_separated holds
X1 misses X2
proof end;

theorem :: TSEP_1:69
canceled;

theorem :: TSEP_1:70
for X being non empty TopSpace
for X1, X2 being non empty closed SubSpace of X holds
( X1 misses X2 iff X1,X2 are_separated )
proof end;

theorem :: TSEP_1:71
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X = X1 union X2 & X1,X2 are_separated holds
X1 is closed SubSpace of X
proof end;

theorem :: TSEP_1:72
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1 union X2 is closed SubSpace of X & X1,X2 are_separated holds
X1 is closed SubSpace of X
proof end;

theorem :: TSEP_1:73
for X being non empty TopSpace
for X1, X2 being non empty open SubSpace of X holds
( X1 misses X2 iff X1,X2 are_separated )
proof end;

theorem :: TSEP_1:74
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X = X1 union X2 & X1,X2 are_separated holds
X1 is open SubSpace of X
proof end;

theorem :: TSEP_1:75
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1 union X2 is open SubSpace of X & X1,X2 are_separated holds
X1 is open SubSpace of X
proof end;

theorem :: TSEP_1:76
for X being non empty TopSpace
for Y, X1, X2 being non empty SubSpace of X st X1 meets Y & X2 meets Y & X1,X2 are_separated holds
( X1 meet Y,X2 meet Y are_separated & Y meet X1,Y meet X2 are_separated )
proof end;

theorem Th77: :: TSEP_1:77
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X
for Y1, Y2 being SubSpace of X st Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & X1,X2 are_separated holds
Y1,Y2 are_separated
proof end;

theorem :: TSEP_1:78
for X being non empty TopSpace
for X1, X2, Y being non empty SubSpace of X st X1 meets X2 & X1,Y are_separated holds
X1 meet X2,Y are_separated
proof end;

theorem :: TSEP_1:79
for X being non empty TopSpace
for X1, X2, Y being non empty SubSpace of X holds
( ( X1,Y are_separated & X2,Y are_separated ) iff X1 union X2,Y are_separated )
proof end;

theorem :: TSEP_1:80
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X holds
( X1,X2 are_separated iff ex Y1, Y2 being non empty closed SubSpace of X st
( X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1 ) )
proof end;

theorem :: TSEP_1:81
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X holds
( X1,X2 are_separated iff ex Y1, Y2 being non empty closed SubSpace of X st
( X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & ( Y1 misses Y2 or Y1 meet Y2 misses X1 union X2 ) ) )
proof end;

theorem :: TSEP_1:82
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X holds
( X1,X2 are_separated iff ex Y1, Y2 being non empty open SubSpace of X st
( X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1 ) )
proof end;

theorem Th83: :: TSEP_1:83
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X holds
( X1,X2 are_separated iff ex Y1, Y2 being non empty open SubSpace of X st
( X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & ( Y1 misses Y2 or Y1 meet Y2 misses X1 union X2 ) ) )
proof end;

definition
let X be TopStruct ;
let X1, X2 be SubSpace of X;
pred X1,X2 are_weakly_separated means :Def9: :: TSEP_1:def 9
 for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds
A1,A2 are_weakly_separated ;
symmetry
for X1, X2 being SubSpace of X st ( for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds
A1,A2 are_weakly_separated ) holds
for A1, A2 being Subset of X st A1 = the carrier of X2 & A2 = the carrier of X1 holds
A1,A2 are_weakly_separated ;
end;

:: deftheorem Def9 defines are_weakly_separated TSEP_1:def 9 :
for X being TopStruct
for X1, X2 being SubSpace of X holds
( X1,X2 are_weakly_separated iff for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds
A1,A2 are_weakly_separated );

notation
let X be TopStruct ;
let X1, X2 be SubSpace of X;
antonym X1,X2 are_not_weakly_separated for X1,X2 are_weakly_separated ;
end;

theorem :: TSEP_1:84
canceled;

theorem Th85: :: TSEP_1:85
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X holds
( ( X1 misses X2 & X1,X2 are_weakly_separated ) iff X1,X2 are_separated )
proof end;

theorem Th86: :: TSEP_1:86
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1 is SubSpace of X2 holds
X1,X2 are_weakly_separated
proof end;

theorem Th87: :: TSEP_1:87
for X being non empty TopSpace
for X1, X2 being closed SubSpace of X holds X1,X2 are_weakly_separated
proof end;

theorem Th88: :: TSEP_1:88
for X being non empty TopSpace
for X1, X2 being open SubSpace of X holds X1,X2 are_weakly_separated
proof end;

theorem :: TSEP_1:89
for X being non empty TopSpace
for X1, X2, Y being non empty SubSpace of X st X1,X2 are_weakly_separated holds
X1 union Y,X2 union Y are_weakly_separated
proof end;

theorem :: TSEP_1:90
for X being non empty TopSpace
for X2, X1, Y1, Y2 being non empty SubSpace of X st Y1 is SubSpace of X2 & Y2 is SubSpace of X1 & X1,X2 are_weakly_separated holds
( X1 union Y1,X2 union Y2 are_weakly_separated & Y1 union X1,Y2 union X2 are_weakly_separated )
proof end;

theorem :: TSEP_1:91
for X being non empty TopSpace
for Y, X1, X2 being non empty SubSpace of X st X1 meets X2 holds
( ( X1,Y are_weakly_separated & X2,Y are_weakly_separated implies X1 meet X2,Y are_weakly_separated ) & ( Y,X1 are_weakly_separated & Y,X2 are_weakly_separated implies Y,X1 meet X2 are_weakly_separated ) )
proof end;

theorem :: TSEP_1:92
for X being non empty TopSpace
for X1, X2, Y being non empty SubSpace of X holds
( ( X1,Y are_weakly_separated & X2,Y are_weakly_separated implies X1 union X2,Y are_weakly_separated ) & ( Y,X1 are_weakly_separated & Y,X2 are_weakly_separated implies Y,X1 union X2 are_weakly_separated ) )
proof end;

theorem :: TSEP_1:93
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1 meets X2 holds
( X1,X2 are_weakly_separated iff ( X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being non empty closed SubSpace of X st
( Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1 union X2) is SubSpace of X2 & ( X1 union X2 is SubSpace of Y1 union Y2 or ex Y being non empty open SubSpace of X st
( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2 ) ) ) ) )
proof end;

theorem :: TSEP_1:94
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X = X1 union X2 & X1 meets X2 holds
( X1,X2 are_weakly_separated iff ( X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being non empty closed SubSpace of X st
( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty open SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) ) ) ) )
proof end;

theorem :: TSEP_1:95
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X = X1 union X2 & X1 misses X2 holds
( X1,X2 are_weakly_separated iff ( X1 is closed SubSpace of X & X2 is closed SubSpace of X ) )
proof end;

theorem :: TSEP_1:96
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1 meets X2 holds
( X1,X2 are_weakly_separated iff ( X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being non empty open SubSpace of X st
( Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1 union X2) is SubSpace of X2 & ( X1 union X2 is SubSpace of Y1 union Y2 or ex Y being non empty closed SubSpace of X st
( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2 ) ) ) ) )
proof end;

theorem :: TSEP_1:97
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X = X1 union X2 & X1 meets X2 holds
( X1,X2 are_weakly_separated iff ( X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being non empty open SubSpace of X st
( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty closed SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) ) ) ) )
proof end;

theorem :: TSEP_1:98
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X = X1 union X2 & X1 misses X2 holds
( X1,X2 are_weakly_separated iff ( X1 is open SubSpace of X & X2 is open SubSpace of X ) )
proof end;

theorem :: TSEP_1:99
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X holds
( X1,X2 are_separated iff ex Y1, Y2 being non empty SubSpace of X st
( Y1,Y2 are_weakly_separated & X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & ( Y1 misses Y2 or Y1 meet Y2 misses X1 union X2 ) ) )
proof end;

theorem :: TSEP_1:100
for T being TopStruct holds T | ([#] T) = TopStruct(# the carrier of T, the topology of T #)
proof end;