:: TSEP_2 semantic presentation

begin

theorem Th1: :: TSEP_2:1
for X being non empty 1-sorted
for A, B being Subset of X holds (A `) \ (B `) = B \ A
proof
let X be non empty 1-sorted ; ::_thesis: for A, B being Subset of X holds (A `) \ (B `) = B \ A
let A, B be Subset of X; ::_thesis: (A `) \ (B `) = B \ A
 (A `) \ (B `) = ([#] X) \ (A \/ (B `)) by XBOOLE_1:41;
then  (A `) \ (B `) = (A `) /\ ((B `) `) by XBOOLE_1:53;
hence  (A `) \ (B `) = B \ A by SUBSET_1:13; ::_thesis: verum
end;

definition
let X be 1-sorted ;
let A1, A2 be Subset of X;
predA1,A2 constitute_a_decomposition  means :Def1: :: TSEP_2:def 1
( A1 misses A2 & A1 \/ A2 = the carrier of X );
symmetry
 for A1, A2 being Subset of X st A1 misses A2 & A1 \/ A2 = the carrier of X holds
( A2 misses A1 & A2 \/ A1 = the carrier of X ) ;
end;

:: deftheorem Def1 defines constitute_a_decomposition TSEP_2:def_1_:_
 for X being 1-sorted
for A1, A2 being Subset of X holds
( A1,A2 constitute_a_decomposition iff ( A1 misses A2 & A1 \/ A2 = the carrier of X ) );

notation
let X be 1-sorted ;
let A1, A2 be Subset of X;
antonym A1,A2 do_not_constitute_a_decomposition for A1,A2 constitute_a_decomposition ;
end;


theorem :: TSEP_2:2
for X being non empty 1-sorted
for A1, A2 being Subset of X holds
( A1,A2 constitute_a_decomposition iff ( A1 misses A2 & A1 \/ A2 = [#] X ) ) by Def1;

theorem Th3: :: TSEP_2:3
for X being non empty 1-sorted
for A1, A2 being Subset of X st A1,A2 constitute_a_decomposition holds
( A1 = A2 ` & A2 = A1 ` )
proof
let X be non empty 1-sorted ; ::_thesis: for A1, A2 being Subset of X st A1,A2 constitute_a_decomposition holds
( A1 = A2 ` & A2 = A1 ` )
let A1, A2 be Subset of X; ::_thesis: ( A1,A2 constitute_a_decomposition implies ( A1 = A2 ` & A2 = A1 ` ) )
assume A1: A1,A2 constitute_a_decomposition ; ::_thesis: ( A1 = A2 ` & A2 = A1 ` )
then A2: A1 misses A2 by Def1;
then A3: A1 c= A2 ` by SUBSET_1:23;
A4: A2 c= A1 ` by A2, SUBSET_1:23;
A5: A1 \/ A2 = [#] X by A1, Def1;
then  A2 ` c= A1 by TDLAT_1:1;
hence  A1 = A2 ` by A3, XBOOLE_0:def_10; ::_thesis: A2 = A1 `
 A1 ` c= A2 by A5, TDLAT_1:1;
hence  A2 = A1 ` by A4, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th4: :: TSEP_2:4
for X being non empty 1-sorted
for A1, A2 being Subset of X st ( A1 = A2 ` or A2 = A1 ` ) holds
A1,A2 constitute_a_decomposition
proof
let X be non empty 1-sorted ; ::_thesis: for A1, A2 being Subset of X st ( A1 = A2 ` or A2 = A1 ` ) holds
A1,A2 constitute_a_decomposition
let A1, A2 be Subset of X; ::_thesis: ( ( A1 = A2 ` or A2 = A1 ` ) implies A1,A2 constitute_a_decomposition )
assume  ( A1 = A2 ` or A2 = A1 ` ) ; ::_thesis: A1,A2 constitute_a_decomposition
then  ( A1 misses A2 & A1 \/ A2 = [#] X ) by TDLAT_1:1, SUBSET_1:23;
hence  A1,A2 constitute_a_decomposition by Def1; ::_thesis: verum
end;

theorem Th5: :: TSEP_2:5
for X being non empty 1-sorted
for A being Subset of X holds A,A ` constitute_a_decomposition
proof
let X be non empty 1-sorted ; ::_thesis: for A being Subset of X holds A,A ` constitute_a_decomposition
let A be Subset of X; ::_thesis: A,A ` constitute_a_decomposition
 ( A misses A ` & A \/ (A `) = [#] X ) by PRE_TOPC:2, XBOOLE_1:79;
hence  A,A ` constitute_a_decomposition by Def1; ::_thesis: verum
end;

theorem :: TSEP_2:6
for X being non empty 1-sorted holds {} X, [#] X constitute_a_decomposition
proof
let X be non empty 1-sorted ; ::_thesis: {} X, [#] X constitute_a_decomposition
 [#] X = ({} X) ` ;
hence  {} X, [#] X constitute_a_decomposition by Th5; ::_thesis: verum
end;

theorem Th7: :: TSEP_2:7
for X being non empty 1-sorted
for A being Subset of X holds A,A do_not_constitute_a_decomposition
proof
let X be non empty 1-sorted ; ::_thesis: for A being Subset of X holds A,A do_not_constitute_a_decomposition
let A be Subset of X; ::_thesis: A,A do_not_constitute_a_decomposition
assume A1: A,A constitute_a_decomposition ; ::_thesis: contradiction
percases ( not A is empty or A is empty ) ;
supposeA2: not A is empty ; ::_thesis: contradiction
 A = A ` by A1, Th3;
then  A misses A by SUBSET_1:23;
then  A /\ A = {} by XBOOLE_0:def_7;
hence  contradiction by A2; ::_thesis: verum
end;
suppose A is empty ; ::_thesis: contradiction
then  {} = A \/ A
.= the carrier of X by A1, Def1 ;
hence  contradiction ; ::_thesis: verum
end;
end;
end;

definition
let X be non empty 1-sorted ;
let A1, A2 be Subset of X;
:: original: constitute_a_decomposition
redefine predA1,A2 constitute_a_decomposition ;
irreflexivity
 for A1 being Subset of X holds (X,b1,b1) by Th7;
end;

theorem Th8: :: TSEP_2:8
for X being non empty 1-sorted
for A1, A, A2 being Subset of X st A1,A constitute_a_decomposition & A,A2 constitute_a_decomposition holds
A1 = A2
proof
let X be non empty 1-sorted ; ::_thesis: for A1, A, A2 being Subset of X st A1,A constitute_a_decomposition & A,A2 constitute_a_decomposition holds
A1 = A2
let A1, A, A2 be Subset of X; ::_thesis: ( A1,A constitute_a_decomposition & A,A2 constitute_a_decomposition implies A1 = A2 )
assume  A1,A constitute_a_decomposition ; ::_thesis: ( not A,A2 constitute_a_decomposition or A1 = A2 )
then A1: A1 = A ` by Th3;
assume  A,A2 constitute_a_decomposition ; ::_thesis: A1 = A2
hence  A1 = A2 by A1, Th3; ::_thesis: verum
end;


theorem Th9: :: TSEP_2:9
for X being non empty TopSpace
for A1, A2 being Subset of X st A1,A2 constitute_a_decomposition holds
( Cl A1, Int A2 constitute_a_decomposition & Int A1, Cl A2 constitute_a_decomposition )
proof
let X be non empty TopSpace; ::_thesis: for A1, A2 being Subset of X st A1,A2 constitute_a_decomposition holds
( Cl A1, Int A2 constitute_a_decomposition & Int A1, Cl A2 constitute_a_decomposition )
let A1, A2 be Subset of X; ::_thesis: ( A1,A2 constitute_a_decomposition implies ( Cl A1, Int A2 constitute_a_decomposition & Int A1, Cl A2 constitute_a_decomposition ) )
assume A1: A1,A2 constitute_a_decomposition ; ::_thesis: ( Cl A1, Int A2 constitute_a_decomposition & Int A1, Cl A2 constitute_a_decomposition )
 Cl A1 = (Int (A1 `)) ` by TDLAT_3:1;
then  Cl A1 = (Int A2) ` by A1, Th3;
hence  Cl A1, Int A2 constitute_a_decomposition by Th4; ::_thesis: Int A1, Cl A2 constitute_a_decomposition
 Int A1 = (Cl (A1 `)) ` by TOPS_1:def_1;
then  Int A1 = (Cl A2) ` by A1, Th3;
hence  Int A1, Cl A2 constitute_a_decomposition by Th4; ::_thesis: verum
end;

theorem :: TSEP_2:10
for X being non empty TopSpace
for A being Subset of X holds
( Cl A, Int (A `) constitute_a_decomposition & Cl (A `), Int A constitute_a_decomposition & Int A, Cl (A `) constitute_a_decomposition & Int (A `), Cl A constitute_a_decomposition )
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X holds
( Cl A, Int (A `) constitute_a_decomposition & Cl (A `), Int A constitute_a_decomposition & Int A, Cl (A `) constitute_a_decomposition & Int (A `), Cl A constitute_a_decomposition )
let A be Subset of X; ::_thesis: ( Cl A, Int (A `) constitute_a_decomposition & Cl (A `), Int A constitute_a_decomposition & Int A, Cl (A `) constitute_a_decomposition & Int (A `), Cl A constitute_a_decomposition )
A1: A,A ` constitute_a_decomposition by Th5;
hence  Cl A, Int (A `) constitute_a_decomposition by Th9; ::_thesis: ( Cl (A `), Int A constitute_a_decomposition & Int A, Cl (A `) constitute_a_decomposition & Int (A `), Cl A constitute_a_decomposition )
A2: A ` ,A constitute_a_decomposition by Th5;
hence  Cl (A `), Int A constitute_a_decomposition by Th9; ::_thesis: ( Int A, Cl (A `) constitute_a_decomposition & Int (A `), Cl A constitute_a_decomposition )
thus  Int A, Cl (A `) constitute_a_decomposition by A2, Th9; ::_thesis: Int (A `), Cl A constitute_a_decomposition
thus  Int (A `), Cl A constitute_a_decomposition by A1, Th9; ::_thesis: verum
end;

theorem Th11: :: TSEP_2:11
for X being non empty TopSpace
for A1, A2 being Subset of X st A1,A2 constitute_a_decomposition holds
( A1 is open iff A2 is closed )
proof
let X be non empty TopSpace; ::_thesis: for A1, A2 being Subset of X st A1,A2 constitute_a_decomposition holds
( A1 is open iff A2 is closed )
let A1, A2 be Subset of X; ::_thesis: ( A1,A2 constitute_a_decomposition implies ( A1 is open iff A2 is closed ) )
assume A1: A1,A2 constitute_a_decomposition ; ::_thesis: ( A1 is open iff A2 is closed )
then  A2 = A1 ` by Th3;
hence  ( A1 is open implies A2 is closed ) by TOPS_1:4; ::_thesis: ( A2 is closed implies A1 is open )
assume A2: A2 is closed ; ::_thesis: A1 is open
 A1 = A2 ` by A1, Th3;
hence  A1 is open by A2, TOPS_1:3; ::_thesis: verum
end;

theorem :: TSEP_2:12
for X being non empty TopSpace
for A1, A2 being Subset of X st A1,A2 constitute_a_decomposition holds
( A1 is closed iff A2 is open ) by Th11;


theorem Th13: :: TSEP_2:13
for X being non empty 1-sorted
for A1, A2, B1, B2 being Subset of X st A1,A2 constitute_a_decomposition & B1,B2 constitute_a_decomposition holds
A1 /\ B1,A2 \/ B2 constitute_a_decomposition
proof
let X be non empty 1-sorted ; ::_thesis: for A1, A2, B1, B2 being Subset of X st A1,A2 constitute_a_decomposition & B1,B2 constitute_a_decomposition holds
A1 /\ B1,A2 \/ B2 constitute_a_decomposition
let A1, A2, B1, B2 be Subset of X; ::_thesis: ( A1,A2 constitute_a_decomposition & B1,B2 constitute_a_decomposition implies A1 /\ B1,A2 \/ B2 constitute_a_decomposition )
assume A1: A1,A2 constitute_a_decomposition ; ::_thesis: ( not B1,B2 constitute_a_decomposition or A1 /\ B1,A2 \/ B2 constitute_a_decomposition )
then  A1 misses A2 by Def1;
then A2: A1 /\ A2 = {} by XBOOLE_0:def_7;
assume A3: B1,B2 constitute_a_decomposition ; ::_thesis: A1 /\ B1,A2 \/ B2 constitute_a_decomposition
then A4: B1 \/ B2 = [#] X by Def1;
 B1 misses B2 by A3, Def1;
then A5: B1 /\ B2 = {} X by XBOOLE_0:def_7;
(A1 /\ B1) /\ (A2 \/ B2) = ((B1 /\ A1) /\ A2) \/ ((A1 /\ B1) /\ B2) by XBOOLE_1:23
.= (B1 /\ (A1 /\ A2)) \/ ((A1 /\ B1) /\ B2) by XBOOLE_1:16
.= (B1 /\ (A1 /\ A2)) \/ (A1 /\ (B1 /\ B2)) by XBOOLE_1:16
.= {} X by A5, A2 ;
then A6: A1 /\ B1 misses A2 \/ B2 by XBOOLE_0:def_7;
(A1 /\ B1) \/ (A2 \/ B2) = (A1 \/ (A2 \/ B2)) /\ (B1 \/ (A2 \/ B2)) by XBOOLE_1:24
.= ((A1 \/ A2) \/ B2) /\ (B1 \/ (B2 \/ A2)) by XBOOLE_1:4
.= ((A1 \/ A2) \/ B2) /\ ((B1 \/ B2) \/ A2) by XBOOLE_1:4
.= (([#] X) \/ B2) /\ (([#] X) \/ A2) by A1, A4, Def1
.= (([#] X) \/ B2) /\ ([#] X) by XBOOLE_1:12
.= ([#] X) /\ ([#] X) by XBOOLE_1:12
.= [#] X ;
hence  A1 /\ B1,A2 \/ B2 constitute_a_decomposition by A6, Def1; ::_thesis: verum
end;

theorem :: TSEP_2:14
for X being non empty 1-sorted
for A1, A2, B1, B2 being Subset of X st A1,A2 constitute_a_decomposition & B1,B2 constitute_a_decomposition holds
A1 \/ B1,A2 /\ B2 constitute_a_decomposition by Th13;

begin


theorem Th15: :: TSEP_2:15
for X being non empty TopSpace
for A1, A2, C1, C2 being Subset of X st A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition holds
( A1,A2 are_weakly_separated iff C1,C2 are_weakly_separated )
proof
let X be non empty TopSpace; ::_thesis: for A1, A2, C1, C2 being Subset of X st A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition holds
( A1,A2 are_weakly_separated iff C1,C2 are_weakly_separated )
let A1, A2, C1, C2 be Subset of X; ::_thesis: ( A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition implies ( A1,A2 are_weakly_separated iff C1,C2 are_weakly_separated ) )
assume  ( A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition ) ; ::_thesis: ( A1,A2 are_weakly_separated iff C1,C2 are_weakly_separated )
then A1: ( C1 = A1 ` & C2 = A2 ` ) by Th3;
thus  ( A1,A2 are_weakly_separated implies C1,C2 are_weakly_separated ) ::_thesis: ( C1,C2 are_weakly_separated implies A1,A2 are_weakly_separated )
proof
assume  A1 \ A2,A2 \ A1 are_separated ; :: according to TSEP_1:def_5 ::_thesis: C1,C2 are_weakly_separated
then  C2 \ C1,(C2 `) \ (C1 `) are_separated by A1, Th1;
then  C2 \ C1,C1 \ C2 are_separated by Th1;
hence  C1,C2 are_weakly_separated by TSEP_1:def_5; ::_thesis: verum
end;
assume  C1,C2 are_weakly_separated ; ::_thesis: A1,A2 are_weakly_separated
then  C1 \ C2,C2 \ C1 are_separated by TSEP_1:def_5;
then  (C2 `) \ (C1 `),C2 \ C1 are_separated by Th1;
then  A2 \ A1,A1 \ A2 are_separated by A1, Th1;
hence  A1,A2 are_weakly_separated by TSEP_1:def_5; ::_thesis: verum
end;

theorem :: TSEP_2:16
for X being non empty TopSpace
for A1, A2 being Subset of X holds
( A1,A2 are_weakly_separated iff A1 ` ,A2 ` are_weakly_separated )
proof
let X be non empty TopSpace; ::_thesis: for A1, A2 being Subset of X holds
( A1,A2 are_weakly_separated iff A1 ` ,A2 ` are_weakly_separated )
let A1, A2 be Subset of X; ::_thesis: ( A1,A2 are_weakly_separated iff A1 ` ,A2 ` are_weakly_separated )
 ( A1,A1 ` constitute_a_decomposition & A2,A2 ` constitute_a_decomposition ) by Th5;
hence  ( A1,A2 are_weakly_separated iff A1 ` ,A2 ` are_weakly_separated ) by Th15; ::_thesis: verum
end;

theorem :: TSEP_2:17
for X being non empty TopSpace
for A1, A2, C1, C2 being Subset of X st A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition & A1,A2 are_separated holds
C1,C2 are_weakly_separated
proof
let X be non empty TopSpace; ::_thesis: for A1, A2, C1, C2 being Subset of X st A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition & A1,A2 are_separated holds
C1,C2 are_weakly_separated
let A1, A2, C1, C2 be Subset of X; ::_thesis: ( A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition & A1,A2 are_separated implies C1,C2 are_weakly_separated )
assume A1: ( A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition ) ; ::_thesis: ( not A1,A2 are_separated or C1,C2 are_weakly_separated )
assume  A1,A2 are_separated ; ::_thesis: C1,C2 are_weakly_separated
then  A1,A2 are_weakly_separated by TSEP_1:46;
hence  C1,C2 are_weakly_separated by A1, Th15; ::_thesis: verum
end;

theorem Th18: :: TSEP_2:18
for X being non empty TopSpace
for A1, A2, C1, C2 being Subset of X st A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition & A1 misses A2 & C1,C2 are_weakly_separated holds
A1,A2 are_separated
proof
let X be non empty TopSpace; ::_thesis: for A1, A2, C1, C2 being Subset of X st A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition & A1 misses A2 & C1,C2 are_weakly_separated holds
A1,A2 are_separated
let A1, A2, C1, C2 be Subset of X; ::_thesis: ( A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition & A1 misses A2 & C1,C2 are_weakly_separated implies A1,A2 are_separated )
assume A1: ( A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition ) ; ::_thesis: ( not A1 misses A2 or not C1,C2 are_weakly_separated or A1,A2 are_separated )
assume A2: A1 /\ A2 = {} ; :: according to XBOOLE_0:def_7 ::_thesis: ( not C1,C2 are_weakly_separated or A1,A2 are_separated )
assume  C1,C2 are_weakly_separated ; ::_thesis: A1,A2 are_separated
then A3: A1,A2 are_weakly_separated by A1, Th15;
 A1 misses A2 by A2, XBOOLE_0:def_7;
hence  A1,A2 are_separated by A3, TSEP_1:46; ::_thesis: verum
end;

theorem :: TSEP_2:19
for X being non empty TopSpace
for A1, A2, C1, C2 being Subset of X st A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition & C1 \/ C2 = the carrier of X & C1,C2 are_weakly_separated holds
A1,A2 are_separated
proof
let X be non empty TopSpace; ::_thesis: for A1, A2, C1, C2 being Subset of X st A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition & C1 \/ C2 = the carrier of X & C1,C2 are_weakly_separated holds
A1,A2 are_separated
let A1, A2, C1, C2 be Subset of X; ::_thesis: ( A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition & C1 \/ C2 = the carrier of X & C1,C2 are_weakly_separated implies A1,A2 are_separated )
assume A1: ( A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition ) ; ::_thesis: ( not C1 \/ C2 = the carrier of X or not C1,C2 are_weakly_separated or A1,A2 are_separated )
assume  C1 \/ C2 = the carrier of X ; ::_thesis: ( not C1,C2 are_weakly_separated or A1,A2 are_separated )
then A2: (C1 \/ C2) ` = {} X by XBOOLE_1:37;
 ( A1 = C1 ` & A2 = C2 ` ) by A1, Th3;
then  A1 /\ A2 = {} by A2, XBOOLE_1:53;
then A3: A1 misses A2 by XBOOLE_0:def_7;
assume  C1,C2 are_weakly_separated ; ::_thesis: A1,A2 are_separated
hence  A1,A2 are_separated by A1, A3, Th18; ::_thesis: verum
end;

theorem :: TSEP_2:20
for X being non empty TopSpace
for A1, A2 being Subset of X st A1,A2 constitute_a_decomposition holds
( A1,A2 are_weakly_separated iff A1,A2 are_separated )
proof
let X be non empty TopSpace; ::_thesis: for A1, A2 being Subset of X st A1,A2 constitute_a_decomposition holds
( A1,A2 are_weakly_separated iff A1,A2 are_separated )
let A1, A2 be Subset of X; ::_thesis: ( A1,A2 constitute_a_decomposition implies ( A1,A2 are_weakly_separated iff A1,A2 are_separated ) )
assume  A1,A2 constitute_a_decomposition ; ::_thesis: ( A1,A2 are_weakly_separated iff A1,A2 are_separated )
then  A1 misses A2 by Def1;
hence  ( A1,A2 are_weakly_separated iff A1,A2 are_separated ) by TSEP_1:46; ::_thesis: verum
end;

theorem Th21: :: TSEP_2:21
for X being non empty TopSpace
for A1, A2 being Subset of X holds
( A1,A2 are_weakly_separated iff (A1 \/ A2) \ A1,(A1 \/ A2) \ A2 are_separated )
proof
let X be non empty TopSpace; ::_thesis: for A1, A2 being Subset of X holds
( A1,A2 are_weakly_separated iff (A1 \/ A2) \ A1,(A1 \/ A2) \ A2 are_separated )
let A1, A2 be Subset of X; ::_thesis: ( A1,A2 are_weakly_separated iff (A1 \/ A2) \ A1,(A1 \/ A2) \ A2 are_separated )
A1: ( (A1 \/ A2) \ A1 = A2 \ A1 & (A1 \/ A2) \ A2 = A1 \ A2 ) by XBOOLE_1:40;
thus  ( A1,A2 are_weakly_separated implies (A1 \/ A2) \ A1,(A1 \/ A2) \ A2 are_separated ) ::_thesis: ( (A1 \/ A2) \ A1,(A1 \/ A2) \ A2 are_separated implies A1,A2 are_weakly_separated )
proof
assume  A1 \ A2,A2 \ A1 are_separated ; :: according to TSEP_1:def_5 ::_thesis: (A1 \/ A2) \ A1,(A1 \/ A2) \ A2 are_separated
hence  (A1 \/ A2) \ A1,(A1 \/ A2) \ A2 are_separated by A1; ::_thesis: verum
end;
assume  (A1 \/ A2) \ A1,(A1 \/ A2) \ A2 are_separated ; ::_thesis: A1,A2 are_weakly_separated
hence  A1,A2 are_weakly_separated by A1, TSEP_1:def_5; ::_thesis: verum
end;

theorem Th22: :: TSEP_2:22
for X being non empty TopSpace
for A1, A2, C1, C2 being Subset of X st C1 c= A1 & C2 c= A2 & C1 \/ C2 = A1 \/ A2 & C1,C2 are_weakly_separated holds
A1,A2 are_weakly_separated
proof
let X be non empty TopSpace; ::_thesis: for A1, A2, C1, C2 being Subset of X st C1 c= A1 & C2 c= A2 & C1 \/ C2 = A1 \/ A2 & C1,C2 are_weakly_separated holds
A1,A2 are_weakly_separated
let A1, A2, C1, C2 be Subset of X; ::_thesis: ( C1 c= A1 & C2 c= A2 & C1 \/ C2 = A1 \/ A2 & C1,C2 are_weakly_separated implies A1,A2 are_weakly_separated )
assume  ( C1 c= A1 & C2 c= A2 ) ; ::_thesis: ( not C1 \/ C2 = A1 \/ A2 or not C1,C2 are_weakly_separated or A1,A2 are_weakly_separated )
then A1: ( (A1 \/ A2) \ A1 c= (A1 \/ A2) \ C1 & (A1 \/ A2) \ A2 c= (A1 \/ A2) \ C2 ) by XBOOLE_1:34;
assume A2: C1 \/ C2 = A1 \/ A2 ; ::_thesis: ( not C1,C2 are_weakly_separated or A1,A2 are_weakly_separated )
assume  C1,C2 are_weakly_separated ; ::_thesis: A1,A2 are_weakly_separated
then  (A1 \/ A2) \ C1,(A1 \/ A2) \ C2 are_separated by A2, Th21;
then  (A1 \/ A2) \ A1,(A1 \/ A2) \ A2 are_separated by A1, CONNSP_1:7;
hence  A1,A2 are_weakly_separated by Th21; ::_thesis: verum
end;

theorem Th23: :: TSEP_2:23
for X being non empty TopSpace
for A1, A2 being Subset of X holds
( A1,A2 are_weakly_separated iff A1 \ (A1 /\ A2),A2 \ (A1 /\ A2) are_separated )
proof
let X be non empty TopSpace; ::_thesis: for A1, A2 being Subset of X holds
( A1,A2 are_weakly_separated iff A1 \ (A1 /\ A2),A2 \ (A1 /\ A2) are_separated )
let A1, A2 be Subset of X; ::_thesis: ( A1,A2 are_weakly_separated iff A1 \ (A1 /\ A2),A2 \ (A1 /\ A2) are_separated )
A1: A2 \ (A1 /\ A2) = A2 \ A1 by XBOOLE_1:47;
A2: A1 \ (A1 /\ A2) = A1 \ A2 by XBOOLE_1:47;
thus  ( A1,A2 are_weakly_separated implies A1 \ (A1 /\ A2),A2 \ (A1 /\ A2) are_separated ) ::_thesis: ( A1 \ (A1 /\ A2),A2 \ (A1 /\ A2) are_separated implies A1,A2 are_weakly_separated )
proof
assume  A1 \ A2,A2 \ A1 are_separated ; :: according to TSEP_1:def_5 ::_thesis: A1 \ (A1 /\ A2),A2 \ (A1 /\ A2) are_separated
hence  A1 \ (A1 /\ A2),A2 \ (A1 /\ A2) are_separated by A2, XBOOLE_1:47; ::_thesis: verum
end;
assume  A1 \ (A1 /\ A2),A2 \ (A1 /\ A2) are_separated ; ::_thesis: A1,A2 are_weakly_separated
hence  A1,A2 are_weakly_separated by A2, A1, TSEP_1:def_5; ::_thesis: verum
end;

theorem Th24: :: TSEP_2:24
for X being non empty TopSpace
for A1, A2, C1, C2 being Subset of X st C1 c= A1 & C2 c= A2 & C1 /\ C2 = A1 /\ A2 & A1,A2 are_weakly_separated holds
C1,C2 are_weakly_separated
proof
let X be non empty TopSpace; ::_thesis: for A1, A2, C1, C2 being Subset of X st C1 c= A1 & C2 c= A2 & C1 /\ C2 = A1 /\ A2 & A1,A2 are_weakly_separated holds
C1,C2 are_weakly_separated
let A1, A2, C1, C2 be Subset of X; ::_thesis: ( C1 c= A1 & C2 c= A2 & C1 /\ C2 = A1 /\ A2 & A1,A2 are_weakly_separated implies C1,C2 are_weakly_separated )
assume  ( C1 c= A1 & C2 c= A2 ) ; ::_thesis: ( not C1 /\ C2 = A1 /\ A2 or not A1,A2 are_weakly_separated or C1,C2 are_weakly_separated )
then A1: ( C1 \ (C1 /\ C2) c= A1 \ (C1 /\ C2) & C2 \ (C1 /\ C2) c= A2 \ (C1 /\ C2) ) by XBOOLE_1:33;
assume A2: C1 /\ C2 = A1 /\ A2 ; ::_thesis: ( not A1,A2 are_weakly_separated or C1,C2 are_weakly_separated )
assume  A1,A2 are_weakly_separated ; ::_thesis: C1,C2 are_weakly_separated
then  A1 \ (C1 /\ C2),A2 \ (C1 /\ C2) are_separated by A2, Th23;
then  C1 \ (C1 /\ C2),C2 \ (C1 /\ C2) are_separated by A1, CONNSP_1:7;
hence  C1,C2 are_weakly_separated by Th23; ::_thesis: verum
end;


theorem Th25: :: TSEP_2:25
for X being non empty TopSpace
for A1, A2 being Subset of X
for X0 being non empty SubSpace of X
for B1, B2 being Subset of X0 st B1 = A1 & B2 = A2 holds
( A1,A2 are_separated iff B1,B2 are_separated )
proof
let X be non empty TopSpace; ::_thesis: for A1, A2 being Subset of X
for X0 being non empty SubSpace of X
for B1, B2 being Subset of X0 st B1 = A1 & B2 = A2 holds
( A1,A2 are_separated iff B1,B2 are_separated )
let A1, A2 be Subset of X; ::_thesis: for X0 being non empty SubSpace of X
for B1, B2 being Subset of X0 st B1 = A1 & B2 = A2 holds
( A1,A2 are_separated iff B1,B2 are_separated )
let X0 be non empty SubSpace of X; ::_thesis: for B1, B2 being Subset of X0 st B1 = A1 & B2 = A2 holds
( A1,A2 are_separated iff B1,B2 are_separated )
let B1, B2 be Subset of X0; ::_thesis: ( B1 = A1 & B2 = A2 implies ( A1,A2 are_separated iff B1,B2 are_separated ) )
assume that
A1: B1 = A1 and
A2: B2 = A2 ; ::_thesis: ( A1,A2 are_separated iff B1,B2 are_separated )
A3: Cl B2 = (Cl A2) /\ ([#] X0) by A2, PRE_TOPC:17;
A4: Cl B1 = (Cl A1) /\ ([#] X0) by A1, PRE_TOPC:17;
thus  ( A1,A2 are_separated implies B1,B2 are_separated ) ::_thesis: ( B1,B2 are_separated implies A1,A2 are_separated )
proof
assume A5: A1,A2 are_separated ; ::_thesis: B1,B2 are_separated
then  A1 misses Cl A2 by CONNSP_1:def_1;
then  A1 /\ (Cl A2) = {} by XBOOLE_0:def_7;
then  B1 /\ (Cl B2) = {} /\ ([#] X0) by A1, A3, XBOOLE_1:16;
then A6: B1 misses Cl B2 by XBOOLE_0:def_7;
 Cl A1 misses A2 by A5, CONNSP_1:def_1;
then  (Cl A1) /\ A2 = {} by XBOOLE_0:def_7;
then  (Cl B1) /\ B2 = {} /\ ([#] X0) by A2, A4, XBOOLE_1:16;
then  Cl B1 misses B2 by XBOOLE_0:def_7;
hence  B1,B2 are_separated by A6, CONNSP_1:def_1; ::_thesis: verum
end;
thus  ( B1,B2 are_separated implies A1,A2 are_separated ) ::_thesis: verum
proof
assume A7: B1,B2 are_separated ; ::_thesis: A1,A2 are_separated
then  (Cl A1) /\ ([#] X0) misses A2 by A2, A4, CONNSP_1:def_1;
then  ((Cl A1) /\ ([#] X0)) /\ A2 = {} by XBOOLE_0:def_7;
then A8: ((Cl A1) /\ A2) /\ ([#] X0) = {} by XBOOLE_1:16;
 A1 misses (Cl A2) /\ ([#] X0) by A1, A3, A7, CONNSP_1:def_1;
then  A1 /\ ((Cl A2) /\ ([#] X0)) = {} by XBOOLE_0:def_7;
then A9: (A1 /\ (Cl A2)) /\ ([#] X0) = {} by XBOOLE_1:16;
 A1 /\ (Cl A2) c= A1 by XBOOLE_1:17;
then  A1 /\ (Cl A2) = {} by A1, A9, XBOOLE_1:1, XBOOLE_1:28;
then A10: A1 misses Cl A2 by XBOOLE_0:def_7;
 (Cl A1) /\ A2 c= A2 by XBOOLE_1:17;
then  (Cl A1) /\ A2 = {} by A2, A8, XBOOLE_1:1, XBOOLE_1:28;
then  Cl A1 misses A2 by XBOOLE_0:def_7;
hence  A1,A2 are_separated by A10, CONNSP_1:def_1; ::_thesis: verum
end;
end;

theorem Th26: :: TSEP_2:26
for X being non empty TopSpace
for A1, A2 being Subset of X
for X0 being non empty SubSpace of X
for B1, B2 being Subset of X0 st B1 = the carrier of X0 /\ A1 & B2 = the carrier of X0 /\ A2 & A1,A2 are_separated holds
B1,B2 are_separated
proof
let X be non empty TopSpace; ::_thesis: for A1, A2 being Subset of X
for X0 being non empty SubSpace of X
for B1, B2 being Subset of X0 st B1 = the carrier of X0 /\ A1 & B2 = the carrier of X0 /\ A2 & A1,A2 are_separated holds
B1,B2 are_separated
let A1, A2 be Subset of X; ::_thesis: for X0 being non empty SubSpace of X
for B1, B2 being Subset of X0 st B1 = the carrier of X0 /\ A1 & B2 = the carrier of X0 /\ A2 & A1,A2 are_separated holds
B1,B2 are_separated
let X0 be non empty SubSpace of X; ::_thesis: for B1, B2 being Subset of X0 st B1 = the carrier of X0 /\ A1 & B2 = the carrier of X0 /\ A2 & A1,A2 are_separated holds
B1,B2 are_separated
let B1, B2 be Subset of X0; ::_thesis: ( B1 = the carrier of X0 /\ A1 & B2 = the carrier of X0 /\ A2 & A1,A2 are_separated implies B1,B2 are_separated )
assume A1: B1 = the carrier of X0 /\ A1 ; ::_thesis: ( not B2 = the carrier of X0 /\ A2 or not A1,A2 are_separated or B1,B2 are_separated )
then reconsider C1 = B1 as Subset of X ;
assume A2: B2 = the carrier of X0 /\ A2 ; ::_thesis: ( not A1,A2 are_separated or B1,B2 are_separated )
then A3: B2 c= A2 by XBOOLE_1:17;
reconsider C2 = B2 as Subset of X by A2;
assume A4: A1,A2 are_separated ; ::_thesis: B1,B2 are_separated
 B1 c= A1 by A1, XBOOLE_1:17;
then  C1,C2 are_separated by A3, A4, CONNSP_1:7;
hence  B1,B2 are_separated by Th25; ::_thesis: verum
end;

theorem Th27: :: TSEP_2:27
for X being non empty TopSpace
for A1, A2 being Subset of X
for X0 being non empty SubSpace of X
for B1, B2 being Subset of X0 st B1 = A1 & B2 = A2 holds
( A1,A2 are_weakly_separated iff B1,B2 are_weakly_separated )
proof
let X be non empty TopSpace; ::_thesis: for A1, A2 being Subset of X
for X0 being non empty SubSpace of X
for B1, B2 being Subset of X0 st B1 = A1 & B2 = A2 holds
( A1,A2 are_weakly_separated iff B1,B2 are_weakly_separated )
let A1, A2 be Subset of X; ::_thesis: for X0 being non empty SubSpace of X
for B1, B2 being Subset of X0 st B1 = A1 & B2 = A2 holds
( A1,A2 are_weakly_separated iff B1,B2 are_weakly_separated )
let X0 be non empty SubSpace of X; ::_thesis: for B1, B2 being Subset of X0 st B1 = A1 & B2 = A2 holds
( A1,A2 are_weakly_separated iff B1,B2 are_weakly_separated )
let B1, B2 be Subset of X0; ::_thesis: ( B1 = A1 & B2 = A2 implies ( A1,A2 are_weakly_separated iff B1,B2 are_weakly_separated ) )
assume A1: ( B1 = A1 & B2 = A2 ) ; ::_thesis: ( A1,A2 are_weakly_separated iff B1,B2 are_weakly_separated )
thus  ( A1,A2 are_weakly_separated implies B1,B2 are_weakly_separated ) ::_thesis: ( B1,B2 are_weakly_separated implies A1,A2 are_weakly_separated )
proof
assume  A1,A2 are_weakly_separated ; ::_thesis: B1,B2 are_weakly_separated
then  A1 \ A2,A2 \ A1 are_separated by TSEP_1:def_5;
then  B1 \ B2,B2 \ B1 are_separated by A1, Th25;
hence  B1,B2 are_weakly_separated by TSEP_1:def_5; ::_thesis: verum
end;
thus  ( B1,B2 are_weakly_separated implies A1,A2 are_weakly_separated ) ::_thesis: verum
proof
assume  B1,B2 are_weakly_separated ; ::_thesis: A1,A2 are_weakly_separated
then  B1 \ B2,B2 \ B1 are_separated by TSEP_1:def_5;
then  A1 \ A2,A2 \ A1 are_separated by A1, Th25;
hence  A1,A2 are_weakly_separated by TSEP_1:def_5; ::_thesis: verum
end;
end;

theorem Th28: :: TSEP_2:28
for X being non empty TopSpace
for A1, A2 being Subset of X
for X0 being non empty SubSpace of X
for B1, B2 being Subset of X0 st B1 = the carrier of X0 /\ A1 & B2 = the carrier of X0 /\ A2 & A1,A2 are_weakly_separated holds
B1,B2 are_weakly_separated
proof
let X be non empty TopSpace; ::_thesis: for A1, A2 being Subset of X
for X0 being non empty SubSpace of X
for B1, B2 being Subset of X0 st B1 = the carrier of X0 /\ A1 & B2 = the carrier of X0 /\ A2 & A1,A2 are_weakly_separated holds
B1,B2 are_weakly_separated
let A1, A2 be Subset of X; ::_thesis: for X0 being non empty SubSpace of X
for B1, B2 being Subset of X0 st B1 = the carrier of X0 /\ A1 & B2 = the carrier of X0 /\ A2 & A1,A2 are_weakly_separated holds
B1,B2 are_weakly_separated
let X0 be non empty SubSpace of X; ::_thesis: for B1, B2 being Subset of X0 st B1 = the carrier of X0 /\ A1 & B2 = the carrier of X0 /\ A2 & A1,A2 are_weakly_separated holds
B1,B2 are_weakly_separated
let B1, B2 be Subset of X0; ::_thesis: ( B1 = the carrier of X0 /\ A1 & B2 = the carrier of X0 /\ A2 & A1,A2 are_weakly_separated implies B1,B2 are_weakly_separated )
assume  ( B1 = the carrier of X0 /\ A1 & B2 = the carrier of X0 /\ A2 ) ; ::_thesis: ( not A1,A2 are_weakly_separated or B1,B2 are_weakly_separated )
then A1: ( B1 \ B2 = the carrier of X0 /\ (A1 \ A2) & B2 \ B1 = the carrier of X0 /\ (A2 \ A1) ) by XBOOLE_1:50;
assume  A1 \ A2,A2 \ A1 are_separated ; :: according to TSEP_1:def_5 ::_thesis: B1,B2 are_weakly_separated
then  B1 \ B2,B2 \ B1 are_separated by A1, Th26;
hence  B1,B2 are_weakly_separated by TSEP_1:def_5; ::_thesis: verum
end;

begin

definition
let X be non empty TopSpace;
let X1, X2 be SubSpace of X;
predX1,X2 constitute_a_decomposition  means :Def2: :: TSEP_2:def 2
 for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds
A1,A2 constitute_a_decomposition ;
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 constitute_a_decomposition ) holds
for A1, A2 being Subset of X st A1 = the carrier of X2 & A2 = the carrier of X1 holds
A1,A2 constitute_a_decomposition ;
end;

:: deftheorem Def2 defines constitute_a_decomposition TSEP_2:def_2_:_
 for X being non empty TopSpace
for X1, X2 being SubSpace of X holds
( X1,X2 constitute_a_decomposition iff for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds
A1,A2 constitute_a_decomposition );

notation
let X be non empty TopSpace;
let X1, X2 be SubSpace of X;
antonym X1,X2 do_not_constitute_a_decomposition for X1,X2 constitute_a_decomposition ;
end;


theorem Th29: :: TSEP_2:29
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X holds
( X1,X2 constitute_a_decomposition iff ( X1 misses X2 & TopStruct(# the carrier of X, the topology of X #) = X1 union X2 ) )
proof
let X be non empty TopSpace; ::_thesis: for X1, X2 being non empty SubSpace of X holds
( X1,X2 constitute_a_decomposition iff ( X1 misses X2 & TopStruct(# the carrier of X, the topology of X #) = X1 union X2 ) )
let X1, X2 be non empty SubSpace of X; ::_thesis: ( X1,X2 constitute_a_decomposition iff ( X1 misses X2 & TopStruct(# the carrier of X, the topology of X #) = X1 union X2 ) )
reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1:1;
thus  ( X1,X2 constitute_a_decomposition implies ( X1 misses X2 & TopStruct(# the carrier of X, the topology of X #) = X1 union X2 ) ) ::_thesis: ( X1 misses X2 & TopStruct(# the carrier of X, the topology of X #) = X1 union X2 implies X1,X2 constitute_a_decomposition )
proof
assume  for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds
A1,A2 constitute_a_decomposition ; :: according to TSEP_2:def_2 ::_thesis: ( X1 misses X2 & TopStruct(# the carrier of X, the topology of X #) = X1 union X2 )
then A1: A1,A2 constitute_a_decomposition ;
then  A1 misses A2 by Def1;
hence  X1 misses X2 by TSEP_1:def_3; ::_thesis: TopStruct(# the carrier of X, the topology of X #) = X1 union X2
 A1 \/ A2 = the carrier of X by A1, Def1;
then A2: the carrier of (X1 union X2) = the carrier of X by TSEP_1:def_2;
 X is SubSpace of X by TSEP_1:2;
hence  TopStruct(# the carrier of X, the topology of X #) = X1 union X2 by A2, TSEP_1:5; ::_thesis: verum
end;
assume A3: X1 misses X2 ; ::_thesis: ( not TopStruct(# the carrier of X, the topology of X #) = X1 union X2 or X1,X2 constitute_a_decomposition )
assume A4: TopStruct(# the carrier of X, the topology of X #) = X1 union X2 ; ::_thesis: X1,X2 constitute_a_decomposition
now__::_thesis:_for_A1,_A2_being_Subset_of_X_st_A1_=_the_carrier_of_X1_&_A2_=_the_carrier_of_X2_holds_
A1,A2_constitute_a_decomposition
let A1, A2 be Subset of X; ::_thesis: ( A1 = the carrier of X1 & A2 = the carrier of X2 implies A1,A2 constitute_a_decomposition )
assume  ( A1 = the carrier of X1 & A2 = the carrier of X2 ) ; ::_thesis: A1,A2 constitute_a_decomposition
then  ( A1 misses A2 & A1 \/ A2 = the carrier of X ) by A3, A4, TSEP_1:def_2, TSEP_1:def_3;
hence  A1,A2 constitute_a_decomposition by Def1; ::_thesis: verum
end;
hence  X1,X2 constitute_a_decomposition by Def2; ::_thesis: verum
end;

theorem Th30: :: TSEP_2:30
for X being non empty TopSpace
for X0 being non empty SubSpace of X holds X0,X0 do_not_constitute_a_decomposition
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty SubSpace of X holds X0,X0 do_not_constitute_a_decomposition
let X0 be non empty SubSpace of X; ::_thesis: X0,X0 do_not_constitute_a_decomposition
reconsider A0 = the carrier of X0 as Subset of X by TSEP_1:1;
now__::_thesis:_ex_A1,_A2_being_Subset_of_X_st_
(_A1_=_the_carrier_of_X0_&_A2_=_the_carrier_of_X0_&_A1,A2_do_not_constitute_a_decomposition_)
take A1 = A0; ::_thesis: ex A2 being Subset of X st
( A1 = the carrier of X0 & A2 = the carrier of X0 & A1,A2 do_not_constitute_a_decomposition )
take A2 = A0; ::_thesis: ( A1 = the carrier of X0 & A2 = the carrier of X0 & A1,A2 do_not_constitute_a_decomposition )
thus  ( A1 = the carrier of X0 & A2 = the carrier of X0 & A1,A2 do_not_constitute_a_decomposition ) by Th7; ::_thesis: verum
end;
hence  X0,X0 do_not_constitute_a_decomposition by Def2; ::_thesis: verum
end;

definition
let X be non empty TopSpace;
let A1, A2 be non empty SubSpace of X;
:: original: constitute_a_decomposition
redefine predA1,A2 constitute_a_decomposition ;
irreflexivity
 for A1 being non empty SubSpace of X holds (X,b1,b1) by Th30;
end;

theorem :: TSEP_2:31
for X being non empty TopSpace
for X1, X0, X2 being non empty SubSpace of X st X1,X0 constitute_a_decomposition & X0,X2 constitute_a_decomposition holds
TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)
proof
let X be non empty TopSpace; ::_thesis: for X1, X0, X2 being non empty SubSpace of X st X1,X0 constitute_a_decomposition & X0,X2 constitute_a_decomposition holds
TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)
let X1, X0, X2 be non empty SubSpace of X; ::_thesis: ( X1,X0 constitute_a_decomposition & X0,X2 constitute_a_decomposition implies TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) )
reconsider A0 = the carrier of X0, A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1:1;
assume  for A1, A0 being Subset of X st A1 = the carrier of X1 & A0 = the carrier of X0 holds
A1,A0 constitute_a_decomposition ; :: according to TSEP_2:def_2 ::_thesis: ( not X0,X2 constitute_a_decomposition or TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) )
then A1: A1,A0 constitute_a_decomposition ;
assume  for A0, A2 being Subset of X st A0 = the carrier of X0 & A2 = the carrier of X2 holds
A0,A2 constitute_a_decomposition ; :: according to TSEP_2:def_2 ::_thesis: TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)
then  A0,A2 constitute_a_decomposition ;
hence  TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) by A1, Th8, TSEP_1:5; ::_thesis: verum
end;

theorem Th32: :: TSEP_2:32
for X being non empty TopSpace
for X1, X2, Y1, Y2 being non empty SubSpace of X st X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition holds
( Y1 union Y2 = TopStruct(# the carrier of X, the topology of X #) iff X1 misses X2 )
proof
let X be non empty TopSpace; ::_thesis: for X1, X2, Y1, Y2 being non empty SubSpace of X st X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition holds
( Y1 union Y2 = TopStruct(# the carrier of X, the topology of X #) iff X1 misses X2 )
let X1, X2, Y1, Y2 be non empty SubSpace of X; ::_thesis: ( X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition implies ( Y1 union Y2 = TopStruct(# the carrier of X, the topology of X #) iff X1 misses X2 ) )
reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1:1;
reconsider B1 = the carrier of Y1, B2 = the carrier of Y2 as Subset of X by TSEP_1:1;
assume that
A1: X1,Y1 constitute_a_decomposition and
A2: X2,Y2 constitute_a_decomposition ; ::_thesis: ( Y1 union Y2 = TopStruct(# the carrier of X, the topology of X #) iff X1 misses X2 )
A3: A2,B2 constitute_a_decomposition by A2, Def2;
then A4: A2 = B2 ` by Th3;
A5: A2 = B2 ` by A3, Th3;
A6: A1,B1 constitute_a_decomposition by A1, Def2;
then A7: A1 = B1 ` by Th3;
thus  ( Y1 union Y2 = TopStruct(# the carrier of X, the topology of X #) implies X1 misses X2 ) ::_thesis: ( X1 misses X2 implies Y1 union Y2 = TopStruct(# the carrier of X, the topology of X #) )
proof
assume  Y1 union Y2 = TopStruct(# the carrier of X, the topology of X #) ; ::_thesis: X1 misses X2
then  B1 \/ B2 = the carrier of X by TSEP_1:def_2;
then  (B1 \/ B2) ` = {} X by XBOOLE_1:37;
then  A1 /\ A2 = {} by A7, A5, XBOOLE_1:53;
then  A1 misses A2 by XBOOLE_0:def_7;
hence  X1 misses X2 by TSEP_1:def_3; ::_thesis: verum
end;
assume  X1 misses X2 ; ::_thesis: Y1 union Y2 = TopStruct(# the carrier of X, the topology of X #)
then  A1 misses A2 by TSEP_1:def_3;
then A8: A1 /\ A2 = {} X by XBOOLE_0:def_7;
 A1 = B1 ` by A6, Th3;
then  (B1 \/ B2) ` = {} X by A4, A8, XBOOLE_1:53;
then  B1 \/ B2 = ({} X) ` ;
then A9: the carrier of (Y1 union Y2) = the carrier of X by TSEP_1:def_2;
 X is SubSpace of X by TSEP_1:2;
hence  Y1 union Y2 = TopStruct(# the carrier of X, the topology of X #) by A9, TSEP_1:5; ::_thesis: verum
end;

theorem Th33: :: TSEP_2:33
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1,X2 constitute_a_decomposition holds
( X1 is open iff X2 is closed )
proof
let X be non empty TopSpace; ::_thesis: for X1, X2 being non empty SubSpace of X st X1,X2 constitute_a_decomposition holds
( X1 is open iff X2 is closed )
let X1, X2 be non empty SubSpace of X; ::_thesis: ( X1,X2 constitute_a_decomposition implies ( X1 is open iff X2 is closed ) )
reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1:1;
assume A1: for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds
A1,A2 constitute_a_decomposition ; :: according to TSEP_2:def_2 ::_thesis: ( X1 is open iff X2 is closed )
thus  ( X1 is open implies X2 is closed ) ::_thesis: ( X2 is closed implies X1 is open )
proof
assume A2: for A1 being Subset of X st A1 = the carrier of X1 holds
A1 is open ; :: according to TSEP_1:def_1 ::_thesis: X2 is closed
now__::_thesis:_for_A2_being_Subset_of_X_st_A2_=_the_carrier_of_X2_holds_
A2_is_closed
let A2 be Subset of X; ::_thesis: ( A2 = the carrier of X2 implies A2 is closed )
assume  A2 = the carrier of X2 ; ::_thesis: A2 is closed
then A3: A1,A2 constitute_a_decomposition by A1;
 A1 is open by A2;
hence  A2 is closed by A3, Th11; ::_thesis: verum
end;
hence  X2 is closed by BORSUK_1:def_11; ::_thesis: verum
end;
assume A4: for A2 being Subset of X st A2 = the carrier of X2 holds
A2 is closed ; :: according to BORSUK_1:def_11 ::_thesis: X1 is open
now__::_thesis:_for_A1_being_Subset_of_X_st_A1_=_the_carrier_of_X1_holds_
A1_is_open
let A1 be Subset of X; ::_thesis: ( A1 = the carrier of X1 implies A1 is open )
assume  A1 = the carrier of X1 ; ::_thesis: A1 is open
then A5: A1,A2 constitute_a_decomposition by A1;
 A2 is closed by A4;
hence  A1 is open by A5, Th11; ::_thesis: verum
end;
hence  X1 is open by TSEP_1:def_1; ::_thesis: verum
end;

theorem :: TSEP_2:34
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1,X2 constitute_a_decomposition holds
( X1 is closed iff X2 is open ) by Th33;

theorem Th35: :: TSEP_2:35
for X being non empty TopSpace
for X1, Y1, X2, Y2 being non empty SubSpace of X st X1 meets Y1 & X1,X2 constitute_a_decomposition & Y1,Y2 constitute_a_decomposition holds
X1 meet Y1,X2 union Y2 constitute_a_decomposition
proof
let X be non empty TopSpace; ::_thesis: for X1, Y1, X2, Y2 being non empty SubSpace of X st X1 meets Y1 & X1,X2 constitute_a_decomposition & Y1,Y2 constitute_a_decomposition holds
X1 meet Y1,X2 union Y2 constitute_a_decomposition
let X1, Y1, X2, Y2 be non empty SubSpace of X; ::_thesis: ( X1 meets Y1 & X1,X2 constitute_a_decomposition & Y1,Y2 constitute_a_decomposition implies X1 meet Y1,X2 union Y2 constitute_a_decomposition )
reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1:1;
reconsider B1 = the carrier of Y1, B2 = the carrier of Y2 as Subset of X by TSEP_1:1;
assume A1: X1 meets Y1 ; ::_thesis: ( not X1,X2 constitute_a_decomposition or not Y1,Y2 constitute_a_decomposition or X1 meet Y1,X2 union Y2 constitute_a_decomposition )
assume  for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds
A1,A2 constitute_a_decomposition ; :: according to TSEP_2:def_2 ::_thesis: ( not Y1,Y2 constitute_a_decomposition or X1 meet Y1,X2 union Y2 constitute_a_decomposition )
then A2: A1,A2 constitute_a_decomposition ;
assume  for B1, B2 being Subset of X st B1 = the carrier of Y1 & B2 = the carrier of Y2 holds
B1,B2 constitute_a_decomposition ; :: according to TSEP_2:def_2 ::_thesis: X1 meet Y1,X2 union Y2 constitute_a_decomposition
then A3: B1,B2 constitute_a_decomposition ;
now__::_thesis:_for_C,_D_being_Subset_of_X_st_C_=_the_carrier_of_(X1_meet_Y1)_&_D_=_the_carrier_of_(X2_union_Y2)_holds_
C,D_constitute_a_decomposition
let C, D be Subset of X; ::_thesis: ( C = the carrier of (X1 meet Y1) & D = the carrier of (X2 union Y2) implies C,D constitute_a_decomposition )
assume  ( C = the carrier of (X1 meet Y1) & D = the carrier of (X2 union Y2) ) ; ::_thesis: C,D constitute_a_decomposition
then  ( C = A1 /\ B1 & D = A2 \/ B2 ) by A1, TSEP_1:def_2, TSEP_1:def_4;
hence  C,D constitute_a_decomposition by A2, A3, Th13; ::_thesis: verum
end;
hence  X1 meet Y1,X2 union Y2 constitute_a_decomposition by Def2; ::_thesis: verum
end;

theorem :: TSEP_2:36
for X being non empty TopSpace
for X2, Y2, X1, Y1 being non empty SubSpace of X st X2 meets Y2 & X1,X2 constitute_a_decomposition & Y1,Y2 constitute_a_decomposition holds
X1 union Y1,X2 meet Y2 constitute_a_decomposition by Th35;

begin

theorem Th37: :: TSEP_2:37
for X being non empty TopSpace
for X1, X2, Y1, Y2 being SubSpace of X st X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition & X1,X2 are_weakly_separated holds
Y1,Y2 are_weakly_separated
proof
let X be non empty TopSpace; ::_thesis: for X1, X2, Y1, Y2 being SubSpace of X st X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition & X1,X2 are_weakly_separated holds
Y1,Y2 are_weakly_separated
let X1, X2, Y1, Y2 be SubSpace of X; ::_thesis: ( X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition & X1,X2 are_weakly_separated implies Y1,Y2 are_weakly_separated )
assume A1: for A1, B1 being Subset of X st A1 = the carrier of X1 & B1 = the carrier of Y1 holds
A1,B1 constitute_a_decomposition ; :: according to TSEP_2:def_2 ::_thesis: ( not X2,Y2 constitute_a_decomposition or not X1,X2 are_weakly_separated or Y1,Y2 are_weakly_separated )
assume A2: for A2, B2 being Subset of X st A2 = the carrier of X2 & B2 = the carrier of Y2 holds
A2,B2 constitute_a_decomposition ; :: according to TSEP_2:def_2 ::_thesis: ( not X1,X2 are_weakly_separated or Y1,Y2 are_weakly_separated )
assume A3: for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds
A1,A2 are_weakly_separated ; :: according to TSEP_1:def_7 ::_thesis: Y1,Y2 are_weakly_separated
now__::_thesis:_for_B1,_B2_being_Subset_of_X_st_B1_=_the_carrier_of_Y1_&_B2_=_the_carrier_of_Y2_holds_
B1,B2_are_weakly_separated
reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1:1;
let B1, B2 be Subset of X; ::_thesis: ( B1 = the carrier of Y1 & B2 = the carrier of Y2 implies B1,B2 are_weakly_separated )
assume  ( B1 = the carrier of Y1 & B2 = the carrier of Y2 ) ; ::_thesis: B1,B2 are_weakly_separated
then A4: ( A1,B1 constitute_a_decomposition & A2,B2 constitute_a_decomposition ) by A1, A2;
 A1,A2 are_weakly_separated by A3;
hence  B1,B2 are_weakly_separated by A4, Th15; ::_thesis: verum
end;
hence  Y1,Y2 are_weakly_separated by TSEP_1:def_7; ::_thesis: verum
end;

theorem :: TSEP_2:38
for X being non empty TopSpace
for X1, X2, Y1, Y2 being non empty SubSpace of X st X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition & X1,X2 are_separated holds
Y1,Y2 are_weakly_separated
proof
let X be non empty TopSpace; ::_thesis: for X1, X2, Y1, Y2 being non empty SubSpace of X st X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition & X1,X2 are_separated holds
Y1,Y2 are_weakly_separated
let X1, X2, Y1, Y2 be non empty SubSpace of X; ::_thesis: ( X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition & X1,X2 are_separated implies Y1,Y2 are_weakly_separated )
assume A1: ( X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition ) ; ::_thesis: ( not X1,X2 are_separated or Y1,Y2 are_weakly_separated )
assume  X1,X2 are_separated ; ::_thesis: Y1,Y2 are_weakly_separated
then  X1,X2 are_weakly_separated by TSEP_1:78;
hence  Y1,Y2 are_weakly_separated by A1, Th37; ::_thesis: verum
end;

theorem Th39: :: TSEP_2:39
for X being non empty TopSpace
for X1, X2, Y1, Y2 being non empty SubSpace of X st X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition & X1 misses X2 & Y1,Y2 are_weakly_separated holds
X1,X2 are_separated
proof
let X be non empty TopSpace; ::_thesis: for X1, X2, Y1, Y2 being non empty SubSpace of X st X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition & X1 misses X2 & Y1,Y2 are_weakly_separated holds
X1,X2 are_separated
let X1, X2, Y1, Y2 be non empty SubSpace of X; ::_thesis: ( X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition & X1 misses X2 & Y1,Y2 are_weakly_separated implies X1,X2 are_separated )
assume A1: ( X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition ) ; ::_thesis: ( not X1 misses X2 or not Y1,Y2 are_weakly_separated or X1,X2 are_separated )
assume A2: X1 misses X2 ; ::_thesis: ( not Y1,Y2 are_weakly_separated or X1,X2 are_separated )
assume  Y1,Y2 are_weakly_separated ; ::_thesis: X1,X2 are_separated
then  X1,X2 are_weakly_separated by A1, Th37;
hence  X1,X2 are_separated by A2, TSEP_1:78; ::_thesis: verum
end;

theorem :: TSEP_2:40
for X being non empty TopSpace
for X1, X2, Y1, Y2 being non empty SubSpace of X st X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition & Y1 union Y2 = TopStruct(# the carrier of X, the topology of X #) & Y1,Y2 are_weakly_separated holds
X1,X2 are_separated
proof
let X be non empty TopSpace; ::_thesis: for X1, X2, Y1, Y2 being non empty SubSpace of X st X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition & Y1 union Y2 = TopStruct(# the carrier of X, the topology of X #) & Y1,Y2 are_weakly_separated holds
X1,X2 are_separated
let X1, X2, Y1, Y2 be non empty SubSpace of X; ::_thesis: ( X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition & Y1 union Y2 = TopStruct(# the carrier of X, the topology of X #) & Y1,Y2 are_weakly_separated implies X1,X2 are_separated )
assume A1: ( X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition ) ; ::_thesis: ( not Y1 union Y2 = TopStruct(# the carrier of X, the topology of X #) or not Y1,Y2 are_weakly_separated or X1,X2 are_separated )
assume  Y1 union Y2 = TopStruct(# the carrier of X, the topology of X #) ; ::_thesis: ( not Y1,Y2 are_weakly_separated or X1,X2 are_separated )
then A2: X1 misses X2 by A1, Th32;
assume  Y1,Y2 are_weakly_separated ; ::_thesis: X1,X2 are_separated
hence  X1,X2 are_separated by A1, A2, Th39; ::_thesis: verum
end;

theorem :: TSEP_2:41
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1,X2 constitute_a_decomposition holds
( X1,X2 are_weakly_separated iff X1,X2 are_separated )
proof
let X be non empty TopSpace; ::_thesis: for X1, X2 being non empty SubSpace of X st X1,X2 constitute_a_decomposition holds
( X1,X2 are_weakly_separated iff X1,X2 are_separated )
let X1, X2 be non empty SubSpace of X; ::_thesis: ( X1,X2 constitute_a_decomposition implies ( X1,X2 are_weakly_separated iff X1,X2 are_separated ) )
assume  X1,X2 constitute_a_decomposition ; ::_thesis: ( X1,X2 are_weakly_separated iff X1,X2 are_separated )
then  X1 misses X2 by Th29;
hence  ( X1,X2 are_weakly_separated iff X1,X2 are_separated ) by TSEP_1:78; ::_thesis: verum
end;

theorem :: TSEP_2:42
for X being non empty TopSpace
for X1, X2, Y1, Y2 being non empty SubSpace of X st Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & Y1 union Y2 = X1 union X2 & Y1,Y2 are_weakly_separated holds
X1,X2 are_weakly_separated
proof
let X be non empty TopSpace; ::_thesis: for X1, X2, Y1, Y2 being non empty SubSpace of X st Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & Y1 union Y2 = X1 union X2 & Y1,Y2 are_weakly_separated holds
X1,X2 are_weakly_separated
let X1, X2, Y1, Y2 be non empty SubSpace of X; ::_thesis: ( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & Y1 union Y2 = X1 union X2 & Y1,Y2 are_weakly_separated implies X1,X2 are_weakly_separated )
reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1:1;
reconsider C1 = the carrier of Y1, C2 = the carrier of Y2 as Subset of X by TSEP_1:1;
assume  ( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 ) ; ::_thesis: ( not Y1 union Y2 = X1 union X2 or not Y1,Y2 are_weakly_separated or X1,X2 are_weakly_separated )
then A1: ( C1 c= A1 & C2 c= A2 ) by TSEP_1:4;
assume A2: Y1 union Y2 = X1 union X2 ; ::_thesis: ( not Y1,Y2 are_weakly_separated or X1,X2 are_weakly_separated )
assume  Y1,Y2 are_weakly_separated ; ::_thesis: X1,X2 are_weakly_separated
then A3: C1,C2 are_weakly_separated by TSEP_1:def_7;
now__::_thesis:_for_A1,_A2_being_Subset_of_X_st_A1_=_the_carrier_of_X1_&_A2_=_the_carrier_of_X2_holds_
A1,A2_are_weakly_separated
let A1, A2 be Subset of X; ::_thesis: ( A1 = the carrier of X1 & A2 = the carrier of X2 implies A1,A2 are_weakly_separated )
assume A4: ( A1 = the carrier of X1 & A2 = the carrier of X2 ) ; ::_thesis: A1,A2 are_weakly_separated
then  A1 \/ A2 = the carrier of (X1 union X2) by TSEP_1:def_2;
then  A1 \/ A2 = C1 \/ C2 by A2, TSEP_1:def_2;
hence  A1,A2 are_weakly_separated by A1, A3, A4, Th22; ::_thesis: verum
end;
hence  X1,X2 are_weakly_separated by TSEP_1:def_7; ::_thesis: verum
end;

theorem :: TSEP_2:43
for X being non empty TopSpace
for X1, X2, Y1, Y2 being non empty SubSpace of X st Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & Y1 meets Y2 & Y1 meet Y2 = X1 meet X2 & X1,X2 are_weakly_separated holds
Y1,Y2 are_weakly_separated
proof
let X be non empty TopSpace; ::_thesis: for X1, X2, Y1, Y2 being non empty SubSpace of X st Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & Y1 meets Y2 & Y1 meet Y2 = X1 meet X2 & X1,X2 are_weakly_separated holds
Y1,Y2 are_weakly_separated
let X1, X2, Y1, Y2 be non empty SubSpace of X; ::_thesis: ( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & Y1 meets Y2 & Y1 meet Y2 = X1 meet X2 & X1,X2 are_weakly_separated implies Y1,Y2 are_weakly_separated )
reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1:1;
reconsider C1 = the carrier of Y1, C2 = the carrier of Y2 as Subset of X by TSEP_1:1;
assume  ( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 ) ; ::_thesis: ( not Y1 meets Y2 or not Y1 meet Y2 = X1 meet X2 or not X1,X2 are_weakly_separated or Y1,Y2 are_weakly_separated )
then A1: ( C1 c= A1 & C2 c= A2 ) by TSEP_1:4;
assume A2: Y1 meets Y2 ; ::_thesis: ( not Y1 meet Y2 = X1 meet X2 or not X1,X2 are_weakly_separated or Y1,Y2 are_weakly_separated )
assume A3: Y1 meet Y2 = X1 meet X2 ; ::_thesis: ( not X1,X2 are_weakly_separated or Y1,Y2 are_weakly_separated )
assume  X1,X2 are_weakly_separated ; ::_thesis: Y1,Y2 are_weakly_separated
then A4: A1,A2 are_weakly_separated by TSEP_1:def_7;
now__::_thesis:_for_C1,_C2_being_Subset_of_X_st_C1_=_the_carrier_of_Y1_&_C2_=_the_carrier_of_Y2_holds_
C1,C2_are_weakly_separated
let C1, C2 be Subset of X; ::_thesis: ( C1 = the carrier of Y1 & C2 = the carrier of Y2 implies C1,C2 are_weakly_separated )
assume A5: ( C1 = the carrier of Y1 & C2 = the carrier of Y2 ) ; ::_thesis: C1,C2 are_weakly_separated
then  C1 meets C2 by A2, TSEP_1:def_3;
then  C1 /\ C2 <> {} by XBOOLE_0:def_7;
then  A1 /\ A2 <> {} by A1, A5, XBOOLE_1:3, XBOOLE_1:27;
then  A1 meets A2 by XBOOLE_0:def_7;
then  X1 meets X2 by TSEP_1:def_3;
then  A1 /\ A2 = the carrier of (X1 meet X2) by TSEP_1:def_4;
then  A1 /\ A2 = C1 /\ C2 by A2, A3, A5, TSEP_1:def_4;
hence  C1,C2 are_weakly_separated by A1, A4, A5, Th24; ::_thesis: verum
end;
hence  Y1,Y2 are_weakly_separated by TSEP_1:def_7; ::_thesis: verum
end;

theorem Th44: :: TSEP_2:44
for X being non empty TopSpace
for X0 being non empty SubSpace of X
for X1, X2 being SubSpace of X
for Y1, Y2 being SubSpace of X0 st the carrier of X1 = the carrier of Y1 & the carrier of X2 = the carrier of Y2 holds
( X1,X2 are_separated iff Y1,Y2 are_separated )
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty SubSpace of X
for X1, X2 being SubSpace of X
for Y1, Y2 being SubSpace of X0 st the carrier of X1 = the carrier of Y1 & the carrier of X2 = the carrier of Y2 holds
( X1,X2 are_separated iff Y1,Y2 are_separated )
let X0 be non empty SubSpace of X; ::_thesis: for X1, X2 being SubSpace of X
for Y1, Y2 being SubSpace of X0 st the carrier of X1 = the carrier of Y1 & the carrier of X2 = the carrier of Y2 holds
( X1,X2 are_separated iff Y1,Y2 are_separated )
let X1, X2 be SubSpace of X; ::_thesis: for Y1, Y2 being SubSpace of X0 st the carrier of X1 = the carrier of Y1 & the carrier of X2 = the carrier of Y2 holds
( X1,X2 are_separated iff Y1,Y2 are_separated )
let X01, X02 be SubSpace of X0; ::_thesis: ( the carrier of X1 = the carrier of X01 & the carrier of X2 = the carrier of X02 implies ( X1,X2 are_separated iff X01,X02 are_separated ) )
reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1:1;
reconsider B1 = the carrier of X01, B2 = the carrier of X02 as Subset of X0 by TSEP_1:1;
assume A1: ( the carrier of X1 = the carrier of X01 & the carrier of X2 = the carrier of X02 ) ; ::_thesis: ( X1,X2 are_separated iff X01,X02 are_separated )
thus  ( X1,X2 are_separated implies X01,X02 are_separated ) ::_thesis: ( X01,X02 are_separated implies X1,X2 are_separated )
proof
assume  X1,X2 are_separated ; ::_thesis: X01,X02 are_separated
then  A1,A2 are_separated by TSEP_1:def_6;
then  for B1, B2 being Subset of X0 st B1 = the carrier of X01 & B2 = the carrier of X02 holds
B1,B2 are_separated by A1, Th25;
hence  X01,X02 are_separated by TSEP_1:def_6; ::_thesis: verum
end;
thus  ( X01,X02 are_separated implies X1,X2 are_separated ) ::_thesis: verum
proof
assume  X01,X02 are_separated ; ::_thesis: X1,X2 are_separated
then  B1,B2 are_separated by TSEP_1:def_6;
then  for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds
A1,A2 are_separated by A1, Th25;
hence  X1,X2 are_separated by TSEP_1:def_6; ::_thesis: verum
end;
end;

theorem :: TSEP_2:45
for X being non empty TopSpace
for X0, X1, X2 being non empty SubSpace of X st X1 meets X0 & X2 meets X0 holds
for Y1, Y2 being SubSpace of X0 st Y1 = X1 meet X0 & Y2 = X2 meet X0 & X1,X2 are_separated holds
Y1,Y2 are_separated
proof
let X be non empty TopSpace; ::_thesis: for X0, X1, X2 being non empty SubSpace of X st X1 meets X0 & X2 meets X0 holds
for Y1, Y2 being SubSpace of X0 st Y1 = X1 meet X0 & Y2 = X2 meet X0 & X1,X2 are_separated holds
Y1,Y2 are_separated
let X0 be non empty SubSpace of X; ::_thesis: for X1, X2 being non empty SubSpace of X st X1 meets X0 & X2 meets X0 holds
for Y1, Y2 being SubSpace of X0 st Y1 = X1 meet X0 & Y2 = X2 meet X0 & X1,X2 are_separated holds
Y1,Y2 are_separated
let X1, X2 be non empty SubSpace of X; ::_thesis: ( X1 meets X0 & X2 meets X0 implies for Y1, Y2 being SubSpace of X0 st Y1 = X1 meet X0 & Y2 = X2 meet X0 & X1,X2 are_separated holds
Y1,Y2 are_separated )
assume A1: ( X1 meets X0 & X2 meets X0 ) ; ::_thesis: for Y1, Y2 being SubSpace of X0 st Y1 = X1 meet X0 & Y2 = X2 meet X0 & X1,X2 are_separated holds
Y1,Y2 are_separated
let Y1, Y2 be SubSpace of X0; ::_thesis: ( Y1 = X1 meet X0 & Y2 = X2 meet X0 & X1,X2 are_separated implies Y1,Y2 are_separated )
assume A2: ( Y1 = X1 meet X0 & Y2 = X2 meet X0 ) ; ::_thesis: ( not X1,X2 are_separated or Y1,Y2 are_separated )
assume  X1,X2 are_separated ; ::_thesis: Y1,Y2 are_separated
then  X1 meet X0,X2 meet X0 are_separated by A1, TSEP_1:70;
hence  Y1,Y2 are_separated by A2, Th44; ::_thesis: verum
end;

theorem :: TSEP_2:46
for X being non empty TopSpace
for X0 being non empty SubSpace of X
for X1, X2 being SubSpace of X
for Y1, Y2 being SubSpace of X0 st the carrier of X1 = the carrier of Y1 & the carrier of X2 = the carrier of Y2 holds
( X1,X2 are_weakly_separated iff Y1,Y2 are_weakly_separated )
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty SubSpace of X
for X1, X2 being SubSpace of X
for Y1, Y2 being SubSpace of X0 st the carrier of X1 = the carrier of Y1 & the carrier of X2 = the carrier of Y2 holds
( X1,X2 are_weakly_separated iff Y1,Y2 are_weakly_separated )
let X0 be non empty SubSpace of X; ::_thesis: for X1, X2 being SubSpace of X
for Y1, Y2 being SubSpace of X0 st the carrier of X1 = the carrier of Y1 & the carrier of X2 = the carrier of Y2 holds
( X1,X2 are_weakly_separated iff Y1,Y2 are_weakly_separated )
let X1, X2 be SubSpace of X; ::_thesis: for Y1, Y2 being SubSpace of X0 st the carrier of X1 = the carrier of Y1 & the carrier of X2 = the carrier of Y2 holds
( X1,X2 are_weakly_separated iff Y1,Y2 are_weakly_separated )
let X01, X02 be SubSpace of X0; ::_thesis: ( the carrier of X1 = the carrier of X01 & the carrier of X2 = the carrier of X02 implies ( X1,X2 are_weakly_separated iff X01,X02 are_weakly_separated ) )
reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;
reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;
reconsider B1 = the carrier of X01 as Subset of X0 by TSEP_1:1;
reconsider B2 = the carrier of X02 as Subset of X0 by TSEP_1:1;
assume A1: ( the carrier of X1 = the carrier of X01 & the carrier of X2 = the carrier of X02 ) ; ::_thesis: ( X1,X2 are_weakly_separated iff X01,X02 are_weakly_separated )
thus  ( X1,X2 are_weakly_separated implies X01,X02 are_weakly_separated ) ::_thesis: ( X01,X02 are_weakly_separated implies X1,X2 are_weakly_separated )
proof
assume  X1,X2 are_weakly_separated ; ::_thesis: X01,X02 are_weakly_separated
then  A1,A2 are_weakly_separated by TSEP_1:def_7;
then  for B1, B2 being Subset of X0 st B1 = the carrier of X01 & B2 = the carrier of X02 holds
B1,B2 are_weakly_separated by A1, Th27;
hence  X01,X02 are_weakly_separated by TSEP_1:def_7; ::_thesis: verum
end;
thus  ( X01,X02 are_weakly_separated implies X1,X2 are_weakly_separated ) ::_thesis: verum
proof
assume  X01,X02 are_weakly_separated ; ::_thesis: X1,X2 are_weakly_separated
then  B1,B2 are_weakly_separated by TSEP_1:def_7;
then  for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds
A1,A2 are_weakly_separated by A1, Th27;
hence  X1,X2 are_weakly_separated by TSEP_1:def_7; ::_thesis: verum
end;
end;

theorem :: TSEP_2:47
for X being non empty TopSpace
for X0, X1, X2 being non empty SubSpace of X st X1 meets X0 & X2 meets X0 holds
for Y1, Y2 being SubSpace of X0 st Y1 = X1 meet X0 & Y2 = X2 meet X0 & X1,X2 are_weakly_separated holds
Y1,Y2 are_weakly_separated
proof
let X be non empty TopSpace; ::_thesis: for X0, X1, X2 being non empty SubSpace of X st X1 meets X0 & X2 meets X0 holds
for Y1, Y2 being SubSpace of X0 st Y1 = X1 meet X0 & Y2 = X2 meet X0 & X1,X2 are_weakly_separated holds
Y1,Y2 are_weakly_separated
let X0 be non empty SubSpace of X; ::_thesis: for X1, X2 being non empty SubSpace of X st X1 meets X0 & X2 meets X0 holds
for Y1, Y2 being SubSpace of X0 st Y1 = X1 meet X0 & Y2 = X2 meet X0 & X1,X2 are_weakly_separated holds
Y1,Y2 are_weakly_separated
let X1, X2 be non empty SubSpace of X; ::_thesis: ( X1 meets X0 & X2 meets X0 implies for Y1, Y2 being SubSpace of X0 st Y1 = X1 meet X0 & Y2 = X2 meet X0 & X1,X2 are_weakly_separated holds
Y1,Y2 are_weakly_separated )
reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1:1;
assume A1: ( X1 meets X0 & X2 meets X0 ) ; ::_thesis: for Y1, Y2 being SubSpace of X0 st Y1 = X1 meet X0 & Y2 = X2 meet X0 & X1,X2 are_weakly_separated holds
Y1,Y2 are_weakly_separated
let Y1, Y2 be SubSpace of X0; ::_thesis: ( Y1 = X1 meet X0 & Y2 = X2 meet X0 & X1,X2 are_weakly_separated implies Y1,Y2 are_weakly_separated )
assume A2: ( Y1 = X1 meet X0 & Y2 = X2 meet X0 ) ; ::_thesis: ( not X1,X2 are_weakly_separated or Y1,Y2 are_weakly_separated )
assume  X1,X2 are_weakly_separated ; ::_thesis: Y1,Y2 are_weakly_separated
then A3: A1,A2 are_weakly_separated by TSEP_1:def_7;
now__::_thesis:_for_C1,_C2_being_Subset_of_X0_st_C1_=_the_carrier_of_Y1_&_C2_=_the_carrier_of_Y2_holds_
C1,C2_are_weakly_separated
let C1, C2 be Subset of X0; ::_thesis: ( C1 = the carrier of Y1 & C2 = the carrier of Y2 implies C1,C2 are_weakly_separated )
assume  ( C1 = the carrier of Y1 & C2 = the carrier of Y2 ) ; ::_thesis: C1,C2 are_weakly_separated
then  ( C1 = the carrier of X0 /\ A1 & C2 = the carrier of X0 /\ A2 ) by A1, A2, TSEP_1:def_4;
hence  C1,C2 are_weakly_separated by A3, Th28; ::_thesis: verum
end;
hence  Y1,Y2 are_weakly_separated by TSEP_1:def_7; ::_thesis: verum
end;