:: by Zbigniew Karno

::

:: Received January 8, 1992

:: Copyright (c) 1992-2012 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 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 )

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 #)

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 #)

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

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 )

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 )

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

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;

::Properties of Closed Subspaces (for the definition see BORSUK_1:def 13).

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 )

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 )

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

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

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

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;

:: 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 );

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;

existence

ex b_{1} being SubSpace of X st

( b_{1} is strict & b_{1} is open )

end;
existence

ex b

( b

proof end;

registration

let X be non empty TopSpace;

existence

ex b_{1} being SubSpace of X st

( b_{1} is strict & b_{1} is open & not b_{1} is empty )

end;
existence

ex b

( b

proof end;

::Properties of Open Subspaces.

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 )

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 )

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

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

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

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;

ex b_{1} being non empty strict SubSpace of X st the carrier of b_{1} = the carrier of X1 \/ the carrier of X2

for b_{1}, b_{2} being non empty strict SubSpace of X st the carrier of b_{1} = the carrier of X1 \/ the carrier of X2 & the carrier of b_{2} = the carrier of X1 \/ the carrier of X2 holds

b_{1} = b_{2}
by Th5;

commutativity

for b_{1} being non empty strict SubSpace of X

for X1, X2 being non empty SubSpace of X st the carrier of b_{1} = the carrier of X1 \/ the carrier of X2 holds

the carrier of b_{1} = the carrier of X2 \/ the carrier of X1
;

end;
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 the carrier of it = the carrier of X1 \/ the carrier of X2;

ex b

proof end;

uniqueness for b

b

commutativity

for b

for X1, X2 being non empty SubSpace of X st the carrier of b

the carrier of b

:: deftheorem Def2 defines union TSEP_1:def 2 :

for X being non empty TopStruct

for X1, X2 being non empty SubSpace of X

for b_{4} being non empty strict SubSpace of X holds

( b_{4} = X1 union X2 iff the carrier of b_{4} = the carrier of X1 \/ the carrier of X2 );

for X being non empty TopStruct

for X1, X2 being non empty SubSpace of X

for b

( b

::Properties of the Union of two Subspaces.

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)

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

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 #) )

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

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

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 ;

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

:: 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 );

for X1, X2 being 1-sorted holds

( X1 misses X2 iff the carrier of X1 misses the carrier of X2 );

definition

let X be non empty TopStruct ;

let X1, X2 be non empty SubSpace of X;

assume A1: X1 meets X2 ;

ex b_{1} being non empty strict SubSpace of X st the carrier of b_{1} = the carrier of X1 /\ the carrier of X2

for b_{1}, b_{2} being non empty strict SubSpace of X st the carrier of b_{1} = the carrier of X1 /\ the carrier of X2 & the carrier of b_{2} = the carrier of X1 /\ the carrier of X2 holds

b_{1} = b_{2}
by Th5;

end;
let X1, X2 be non empty SubSpace of X;

assume A1: X1 meets X2 ;

func X1 meet X2 -> non empty strict SubSpace of X means :Def4: :: TSEP_1:def 4

the carrier of it = the carrier of X1 /\ the carrier of X2;

existence the carrier of it = the carrier of X1 /\ the carrier of X2;

ex b

proof end;

uniqueness for b

b

:: deftheorem Def4 defines meet TSEP_1:def 4 :

for X being non empty TopStruct

for X1, X2 being non empty SubSpace of X st X1 meets X2 holds

for b_{4} being non empty strict SubSpace of X holds

( b_{4} = X1 meet X2 iff the carrier of b_{4} = the carrier of X1 /\ the carrier of X2 );

for X being non empty TopStruct

for X1, X2 being non empty SubSpace of X st X1 meets X2 holds

for b

( b

::Properties of the Meet of two Subspaces.

theorem Th26: :: TSEP_1:26

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) ) )

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 Th27: :: TSEP_1:27

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 )

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:28

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 ) )

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:29

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

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:30

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

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;

::Connections between the Union and the Meet.

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 meet X2 is SubSpace of X1 union X2

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:32

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) )

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:33

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) )

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;
let A1, A2 be Subset of X;

antonym A1,A2 are_not_separated for A1,A2 are_separated ;

::Properties of Separated Subsets of Topological Spaces.

theorem Th34: :: TSEP_1:34

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 )

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 Th35: :: TSEP_1:35

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 )

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 Th36: :: TSEP_1:36

for X being TopSpace

for A1, A2 being Subset of X st A1 misses A2 & A1 is open holds

A1 misses Cl A2

for A1, A2 being Subset of X st A1 misses A2 & A1 is open holds

A1 misses Cl A2

proof end;

theorem Th37: :: TSEP_1:37

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 )

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 Th38: :: TSEP_1:38

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 )

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 Th39: :: TSEP_1:39

for X being TopSpace

for A1, A2, C being Subset of X st A1,A2 are_separated holds

A1 /\ C,A2 /\ C are_separated

for A1, A2, C being Subset of X st A1,A2 are_separated holds

A1 /\ C,A2 /\ C are_separated

proof end;

theorem Th40: :: TSEP_1:40

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

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 Th41: :: TSEP_1:41

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 )

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 Th42: :: TSEP_1:42

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 ) )

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;

::First Characterization of Separated Subsets of Topological Spaces.

theorem Th43: :: TSEP_1:43

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 ) )

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 Th44: :: TSEP_1:44

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 ) )

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;

::Second Characterization of Separated Subsets of Topological Spaces.

theorem Th45: :: TSEP_1:45

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 ) )

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;

symmetry

for A1, A2 being Subset of X st A1 \ A2,A2 \ A1 are_separated holds

A2 \ A1,A1 \ A2 are_separated ;

end;
let A1, A2 be Subset of X;

symmetry

for A1, A2 being Subset of X st A1 \ A2,A2 \ A1 are_separated holds

A2 \ A1,A1 \ A2 are_separated ;

:: deftheorem Def5 defines are_weakly_separated TSEP_1:def 5 :

for X being TopStruct

for A1, A2 being Subset of X holds

( A1,A2 are_weakly_separated iff A1 \ A2,A2 \ A1 are_separated );

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;
let A1, A2 be Subset of X;

antonym A1,A2 are_not_weakly_separated for A1,A2 are_weakly_separated ;

::Properties of Weakly Separated Subsets of Topological Spaces.

theorem Th46: :: TSEP_1:46

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 )

for A1, A2 being Subset of X holds

( ( A1 misses A2 & A1,A2 are_weakly_separated ) iff A1,A2 are_separated )

proof end;

theorem Th48: :: TSEP_1:48

for X being TopSpace

for A1, A2 being Subset of X st A1 is closed & A2 is closed holds

A1,A2 are_weakly_separated

for A1, A2 being Subset of X st A1 is closed & A2 is closed holds

A1,A2 are_weakly_separated

proof end;

theorem Th49: :: TSEP_1:49

for X being TopSpace

for A1, A2 being Subset of X st A1 is open & A2 is open holds

A1,A2 are_weakly_separated

for A1, A2 being Subset of X st A1 is open & A2 is open holds

A1,A2 are_weakly_separated

proof end;

::Extension Theorems for Weakly Separated Subsets.

theorem Th50: :: TSEP_1:50

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

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 Th51: :: TSEP_1:51

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

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 Th52: :: TSEP_1:52

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

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 Th53: :: TSEP_1:53

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

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;

::First Characterization of Weakly Separated Subsets of Topological Spaces.

theorem Th54: :: TSEP_1:54

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 ) )

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 Th55: :: TSEP_1:55

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 ) ) )

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 Th56: :: TSEP_1:56

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 ) )

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 Th57: :: TSEP_1:57

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 ) ) )

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;

::Second Characterization of Weakly Separated Subsets of Topological Spaces.

theorem Th58: :: TSEP_1:58

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 ) )

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 Th59: :: TSEP_1:59

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 ) ) )

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 Th60: :: TSEP_1:60

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 ) )

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 Th61: :: TSEP_1:61

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 ) ) )

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;

::A Characterization of Separated Subsets by means of Weakly Separated ones.

theorem Th62: :: TSEP_1:62

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 ) )

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;

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;
let X1, X2 be SubSpace of X;

pred X1,X2 are_separated means :Def6: :: TSEP_1:def 6

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 A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds

A1,A2 are_separated ;

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 ;

:: deftheorem Def6 defines are_separated TSEP_1:def 6 :

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 );

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;
let X1, X2 be SubSpace of X;

antonym X1,X2 are_not_separated for X1,X2 are_separated ;

::Properties of Separated Subspaces of Topological Spaces.

theorem :: TSEP_1:63

for X being non empty TopSpace

for X1, X2 being non empty SubSpace of X st X1,X2 are_separated holds

X1 misses X2

for X1, X2 being non empty SubSpace of X st X1,X2 are_separated holds

X1 misses X2

proof end;

theorem :: TSEP_1:64

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 )

for X1, X2 being non empty closed SubSpace of X holds

( X1 misses X2 iff X1,X2 are_separated )

proof end;

theorem :: TSEP_1:65

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

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:66

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

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:67

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 )

for X1, X2 being non empty open SubSpace of X holds

( X1 misses X2 iff X1,X2 are_separated )

proof end;

theorem :: TSEP_1:68

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

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:69

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

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;

::Restriction Theorems for Separated Subspaces.

theorem :: TSEP_1:70

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 )

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 Th71: :: TSEP_1:71

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

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:72

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

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:73

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 )

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:74

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 ) )

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;

::First Characterization of Separated Subspaces of Topological Spaces.

theorem :: TSEP_1:75

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 ) ) )

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:76

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 ) )

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;

::Second Characterization of Separated Subspaces of Topological Spaces.

theorem Th77: :: TSEP_1:77

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 ) ) )

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;

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;
let X1, X2 be SubSpace of X;

pred X1,X2 are_weakly_separated means :Def7: :: TSEP_1:def 7

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 A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds

A1,A2 are_weakly_separated ;

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 ;

:: deftheorem Def7 defines are_weakly_separated TSEP_1:def 7 :

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 );

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;
let X1, X2 be SubSpace of X;

antonym X1,X2 are_not_weakly_separated for X1,X2 are_weakly_separated ;

::Properties of Weakly Separated Subspaces of Topological Spaces.

theorem Th78: :: TSEP_1:78

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 )

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 Th79: :: TSEP_1:79

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

for X1, X2 being non empty SubSpace of X st X1 is SubSpace of X2 holds

X1,X2 are_weakly_separated

proof end;

theorem Th80: :: TSEP_1:80

for X being non empty TopSpace

for X1, X2 being closed SubSpace of X holds X1,X2 are_weakly_separated

for X1, X2 being closed SubSpace of X holds X1,X2 are_weakly_separated

proof end;

::Extension Theorems for Weakly Separated Subspaces.

theorem :: TSEP_1:82

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

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:83

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 )

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:84

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 ) )

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:85

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 ) )

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;

::First Characterization of Weakly Separated Subspaces of Topological Spaces.

theorem :: TSEP_1:86

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 ) ) ) ) )

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:87

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 ) ) ) ) )

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:88

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 ) )

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;

::Second Characterization of Weakly Separated Subspaces of Topological Spaces.

theorem :: TSEP_1:89

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 ) ) ) ) )

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:90

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 ) ) ) ) )

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:91

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 ) )

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;

::A Characterization of Separated Subspaces by means of Weakly Separated ones.

theorem :: TSEP_1:92

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 ) ) )

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;