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