let TM be metrizable TopSpace; :: thesis: for M being Subset of TM
for A1, A2 being closed Subset of TM
for V1, V2 being open Subset of TM st A1 c= V1 & A2 c= V2 & Cl V1 misses Cl V2 holds
for mV1, mV2, mL being Subset of (TM | M) st mV1 = M /\ (Cl V1) & mV2 = M /\ (Cl V2) & mL separates mV1,mV2 holds
ex L being Subset of TM st
( L separates A1,A2 & M /\ L c= mL )
let M be Subset of TM; :: thesis: for A1, A2 being closed Subset of TM
for V1, V2 being open Subset of TM st A1 c= V1 & A2 c= V2 & Cl V1 misses Cl V2 holds
for mV1, mV2, mL being Subset of (TM | M) st mV1 = M /\ (Cl V1) & mV2 = M /\ (Cl V2) & mL separates mV1,mV2 holds
ex L being Subset of TM st
( L separates A1,A2 & M /\ L c= mL )
let A1, A2 be closed Subset of TM; :: thesis: for V1, V2 being open Subset of TM st A1 c= V1 & A2 c= V2 & Cl V1 misses Cl V2 holds
for mV1, mV2, mL being Subset of (TM | M) st mV1 = M /\ (Cl V1) & mV2 = M /\ (Cl V2) & mL separates mV1,mV2 holds
ex L being Subset of TM st
( L separates A1,A2 & M /\ L c= mL )
let V1, V2 be open Subset of TM; :: thesis: ( A1 c= V1 & A2 c= V2 & Cl V1 misses Cl V2 implies for mV1, mV2, mL being Subset of (TM | M) st mV1 = M /\ (Cl V1) & mV2 = M /\ (Cl V2) & mL separates mV1,mV2 holds
ex L being Subset of TM st
( L separates A1,A2 & M /\ L c= mL ) )
assume that
A1: A1 c= V1 and
A2: A2 c= V2 and
A3: Cl V1 misses Cl V2 ; :: thesis: for mV1, mV2, mL being Subset of (TM | M) st mV1 = M /\ (Cl V1) & mV2 = M /\ (Cl V2) & mL separates mV1,mV2 holds
ex L being Subset of TM st
( L separates A1,A2 & M /\ L c= mL )
set TMM = TM | M;
let mV1, mV2, mL be Subset of (TM | M); :: thesis: ( mV1 = M /\ (Cl V1) & mV2 = M /\ (Cl V2) & mL separates mV1,mV2 implies ex L being Subset of TM st
( L separates A1,A2 & M /\ L c= mL ) )
assume that
A4: mV1 = M /\ (Cl V1) and
A5: mV2 = M /\ (Cl V2) and
A6: mL separates mV1,mV2 ; :: thesis: ex L being Subset of TM st
( L separates A1,A2 & M /\ L c= mL )
A7: V2 /\ M c= mV2 by A5, PRE_TOPC:18, XBOOLE_1:26;
consider U9, W9 being open Subset of (TM | M) such that
A8: mV1 c= U9 and
A9: mV2 c= W9 and
A10: U9 misses W9 and
A11: mL = (U9 \/ W9) ` by A6;
A12: [#] (TM | M) = M by PRE_TOPC:def 5;
then reconsider u = U9, w = W9 as Subset of TM by XBOOLE_1:1;
set u1 = u \/ A1;
set w1 = w \/ A2;
A13: mV2 /\ u c= U9 /\ W9 by A9, XBOOLE_1:26;
U9,W9 are_separated by A10, TSEP_1:37;
then A14: u,w are_separated by CONNSP_1:5;
V2 /\ u = V2 /\ (M /\ u) by A12, XBOOLE_1:28
.= (V2 /\ M) /\ u by XBOOLE_1:16 ;
then V2 /\ u c= mV2 /\ u by A7, XBOOLE_1:26;
then V2 /\ u c= U9 /\ W9 by A13;
then V2 /\ u c= {} by A10;
then V2 /\ u = {} ;
then V2 misses u ;
then A15: V2 misses Cl u by TSEP_1:36;
A16: Cl (u \/ A1) misses w \/ A2

proof

assume Cl (u \/ A1) meets w \/ A2 ; :: thesis: contradiction
then consider x being object such that
A17: ( x in Cl (u \/ A1) & x in w \/ A2 ) by XBOOLE_0:3;
A18: Cl (u \/ A1) = (Cl u) \/ (Cl A1) by PRE_TOPC:20;

per cases ( ( x in Cl u & x in w ) or ( x in Cl u & x in A2 ) or ( x in Cl A1 & x in w ) or ( x in Cl A1 & x in A2 ) ) by A17, A18, XBOOLE_0:def 3;

suppose ( x in Cl u & x in w ) ; :: thesis: contradiction

then w meets Cl u by XBOOLE_0:3;
hence contradiction by A14, CONNSP_1:def 1; :: thesis: verum

end;

suppose ( x in Cl u & x in A2 ) ; :: thesis: contradiction

hence contradiction by A2, A15, XBOOLE_0:3; :: thesis: verum

end;

suppose A19: ( x in Cl A1 & x in w ) ; :: thesis: contradiction

Cl A1 c= Cl V1 by A1, PRE_TOPC:19;
then x in mV1 by A4, A12, A19, XBOOLE_0:def 4;
hence contradiction by A8, A10, A19, XBOOLE_0:3; :: thesis: verum

end;

suppose A20: ( x in Cl A1 & x in A2 ) ; :: thesis: contradiction

A21: ( Cl A1 c= Cl V1 & V2 c= Cl V2 ) by A1, PRE_TOPC:18, PRE_TOPC:19;
x in V2 by A2, A20;
hence contradiction by A3, A20, A21, XBOOLE_0:3; :: thesis: verum

end;

end;

end;

A22: V1 /\ M c= mV1 by A4, PRE_TOPC:18, XBOOLE_1:26;
A23: mV1 /\ w c= U9 /\ W9 by A8, XBOOLE_1:26;
V1 /\ w = V1 /\ (M /\ w) by A12, XBOOLE_1:28
.= (V1 /\ M) /\ w by XBOOLE_1:16 ;
then V1 /\ w c= mV1 /\ w by A22, XBOOLE_1:26;
then V1 /\ w c= U9 /\ W9 by A23;
then V1 /\ w c= {} by A10;
then V1 /\ w = {} ;
then V1 misses w ;
then A24: V1 misses Cl w by TSEP_1:36;
Cl (w \/ A2) misses u \/ A1

proof

assume Cl (w \/ A2) meets u \/ A1 ; :: thesis: contradiction
then consider x being object such that
A25: ( x in Cl (w \/ A2) & x in u \/ A1 ) by XBOOLE_0:3;
A26: Cl (w \/ A2) = (Cl w) \/ (Cl A2) by PRE_TOPC:20;

per cases ( ( x in Cl w & x in u ) or ( x in Cl w & x in A1 ) or ( x in Cl A2 & x in u ) or ( x in Cl A2 & x in A1 ) ) by A25, A26, XBOOLE_0:def 3;

suppose ( x in Cl w & x in u ) ; :: thesis: contradiction

then Cl w meets u by XBOOLE_0:3;
hence contradiction by A14, CONNSP_1:def 1; :: thesis: verum

end;

suppose ( x in Cl w & x in A1 ) ; :: thesis: contradiction

hence contradiction by A1, A24, XBOOLE_0:3; :: thesis: verum

end;

suppose A27: ( x in Cl A2 & x in u ) ; :: thesis: contradiction

Cl A2 c= Cl V2 by A2, PRE_TOPC:19;
then x in mV2 by A5, A12, A27, XBOOLE_0:def 4;
hence contradiction by A9, A10, A27, XBOOLE_0:3; :: thesis: verum

end;

suppose A28: ( x in Cl A2 & x in A1 ) ; :: thesis: contradiction

A29: ( Cl A2 c= Cl V2 & V1 c= Cl V1 ) by A2, PRE_TOPC:18, PRE_TOPC:19;
x in V1 by A1, A28;
hence contradiction by A3, A28, A29, XBOOLE_0:3; :: thesis: verum

end;

end;

end;

then u \/ A1,w \/ A2 are_separated by A16, CONNSP_1:def 1;
then consider U1, W1 being open Subset of TM such that
A30: u \/ A1 c= U1 and
A31: w \/ A2 c= W1 and
A32: U1 misses W1 by Lm13;
take L = (U1 \/ W1) ` ; :: thesis: ( L separates A1,A2 & M /\ L c= mL )
A2 c= w \/ A2 by XBOOLE_1:7;
then A33: A2 c= W1 by A31;
w c= w \/ A2 by XBOOLE_1:7;
then A34: w c= W1 by A31;
u c= u \/ A1 by XBOOLE_1:7;
then u c= U1 by A30;
then A35: u \/ w c= U1 \/ W1 by A34, XBOOLE_1:13;
A1 c= u \/ A1 by XBOOLE_1:7;
then A1 c= U1 by A30;
hence L separates A1,A2 by A32, A33; :: thesis: M /\ L c= mL
A36: ([#] (TM | M)) \ (U9 \/ W9) = mL by A11;
M /\ L = (M /\ ([#] TM)) \ (U1 \/ W1) by XBOOLE_1:49
.= M \ (U1 \/ W1) by XBOOLE_1:28 ;
then M /\ L c= M \ (U9 \/ W9) by A35, XBOOLE_1:34;
hence M /\ L c= mL by A36, PRE_TOPC:def 5; :: thesis: verum