let X be non empty TopSpace; :: thesis: ( X is locally_connected & X is normal implies for A, B being Subset of X st A <> {} & B <> {} & A is closed & B is closed & A misses B & A is connected & B is connected holds
ex R, S being Subset of X st
( R is connected & S is connected & R is open & S is open & A c= R & B c= S & R misses S ) )
assume A1: ( X is locally_connected & X is normal ) ; :: thesis: for A, B being Subset of X st A <> {} & B <> {} & A is closed & B is closed & A misses B & A is connected & B is connected holds
ex R, S being Subset of X st
( R is connected & S is connected & R is open & S is open & A c= R & B c= S & R misses S )
let A, B be Subset of X; :: thesis: ( A <> {} & B <> {} & A is closed & B is closed & A misses B & A is connected & B is connected implies ex R, S being Subset of X st
( R is connected & S is connected & R is open & S is open & A c= R & B c= S & R misses S ) )
assume that
A2: ( A <> {} & B <> {} ) and
A3: ( A is closed & B is closed ) and
A4: A misses B ; :: thesis: ( not A is connected or not B is connected or ex R, S being Subset of X st
( R is connected & S is connected & R is open & S is open & A c= R & B c= S & R misses S ) )
assume A5: ( A is connected & B is connected ) ; :: thesis: ex R, S being Subset of X st
( R is connected & S is connected & R is open & S is open & A c= R & B c= S & R misses S )
A6: A c= B ` by A4, SUBSET_1:43;
A7: B ` is open by A3, TOPS_1:29;
B = ([#] X) \ (([#] X) \ B) by PRE_TOPC:22;
then ([#] X) \ B <> [#] X by A2, PRE_TOPC:23;
then consider G being Subset of X such that
A8: ( G is open & A c= G ) and
A9: Cl G c= B ` by A1, A2, A3, A6, A7, Th26;
A10: Cl G misses B by A9, SUBSET_1:43;
A <> {} X by A2;
then consider x being Point of X such that
A11: x in A by PRE_TOPC:41;
A12: x in G by A8, A11;
reconsider G = G as non empty Subset of X by A2, A8;
x in [#] (X | G) by A12, PRE_TOPC:def 10;
then reconsider y = x as Point of (X | G) ;
set H = Component_of y;
reconsider H1 = Component_of y as Subset of X by PRE_TOPC:39;
take R = H1; :: thesis: ex S being Subset of X st
( R is connected & S is connected & R is open & S is open & A c= R & B c= S & R misses S )
A13: Component_of y is_a_component_of X | G by CONNSP_1:43;
A14: Component_of y is connected by CONNSP_1:41;
A15: H1 is_a_component_of G by A13, CONNSP_1:def 6;
A c= [#] (X | G) by A8, PRE_TOPC:def 10;
then reconsider A1 = A as Subset of (X | G) ;
A1 is connected by A5, CONNSP_1:24;
then ( A1 misses Component_of y or A1 c= Component_of y ) by A13, CONNSP_1:38;
then A16: ( A1 /\ (Component_of y) = {} or A1 c= Component_of y ) by XBOOLE_0:def 7;
A17: y in Component_of y by CONNSP_1:40;
B <> {} X by A2;
then consider z being Point of X such that
A18: z in B by PRE_TOPC:41;
A19: B c= (Cl G) ` by A10, SUBSET_1:43;
then A20: z in (Cl G) ` by A18;
reconsider C = (Cl G) ` as non empty Subset of X by A18, A19;
z in [#] (X | C) by A20, PRE_TOPC:def 10;
then reconsider z1 = z as Point of (X | C) ;
set V = Component_of z1;
reconsider V1 = Component_of z1 as Subset of X by PRE_TOPC:39;
take S = V1; :: thesis: ( R is connected & S is connected & R is open & S is open & A c= R & B c= S & R misses S )
A21: Component_of z1 is_a_component_of X | C by CONNSP_1:43;
Cl G = Cl (Cl G) ;
then Cl G is closed by PRE_TOPC:52;
then A22: (Cl G) ` is open by TOPS_1:29;
A23: V1 is_a_component_of (Cl G) ` by A21, CONNSP_1:def 6;
A24: Component_of z1 is connected by CONNSP_1:41;
B c= [#] (X | ((Cl G) ` )) by A19, PRE_TOPC:def 10;
then reconsider B1 = B as Subset of (X | ((Cl G) ` )) ;
B1 is connected by A5, CONNSP_1:24;
then ( B1 misses Component_of z1 or B1 c= Component_of z1 ) by A21, CONNSP_1:38;
then A25: ( B1 /\ (Component_of z1) = {} or B1 c= Component_of z1 ) by XBOOLE_0:def 7;
A26: z1 in Component_of z1 by CONNSP_1:40;
Component_of y c= [#] (X | G) ;
then A27: R c= G by PRE_TOPC:def 10;
G c= Cl G by PRE_TOPC:48;
then A28: R c= Cl G by A27, XBOOLE_1:1;
Component_of z1 c= [#] (X | ((Cl G) ` )) ;
then S c= (Cl G) ` by PRE_TOPC:def 10;
then A29: R /\ S c= (Cl G) /\ ((Cl G) ` ) by A28, XBOOLE_1:27;
Cl G misses (Cl G) ` by XBOOLE_1:79;
then R /\ S c= {} X by A29, XBOOLE_0:def 7;
then R /\ S = {} ;
hence ( R is connected & S is connected & R is open & S is open & A c= R & B c= S & R misses S ) by A1, A8, A11, A14, A15, A16, A17, A18, A22, A23, A24, A25, A26, Th24, CONNSP_1:24, XBOOLE_0:def 4, XBOOLE_0:def 7; :: thesis: verum