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 that

A1: X is locally_connected and

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

A3: A <> {} and

A4: B <> {} and

A5: A is closed and

A6: ( B is closed & 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 ) )

B = ([#] X) \ (([#] X) \ B) by PRE_TOPC:3;

then A7: ([#] X) \ B <> [#] X by A4, PRE_TOPC:4;

A <> {} X by A3;

then consider x being Point of X such that

A8: x in A by PRE_TOPC:12;

( A c= B ` & B ` is open ) by A6, SUBSET_1:23;

then consider G being Subset of X such that

A9: G is open and

A10: A c= G and

A11: Cl G c= B ` by A2, A3, A5, A7, Th20;

A12: Cl G misses B by A11, SUBSET_1:23;

A13: x in G by A10, A8;

reconsider G = G as non empty Subset of X by A3, A10;

x in [#] (X | G) by A13, PRE_TOPC:def 5;

then reconsider y = x as Point of (X | G) ;

A14: Cl G misses (Cl G) ` by XBOOLE_1:79;

assume that

A15: A is connected and

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

set H = Component_of y;

reconsider H1 = Component_of y as Subset of X by PRE_TOPC:11;

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 )

A17: Component_of y is a_component by CONNSP_1:40;

then A18: H1 is_a_component_of G by CONNSP_1:def 6;

A c= [#] (X | G) by A10, PRE_TOPC:def 5;

then reconsider A1 = A as Subset of (X | G) ;

A19: ( Component_of y is connected & y in Component_of y ) by CONNSP_1:38;

A1 is connected by A15, CONNSP_1:23;

then ( A1 misses Component_of y or A1 c= Component_of y ) by A17, CONNSP_1:36;

then A20: ( A1 /\ (Component_of y) = {} or A1 c= Component_of y ) by XBOOLE_0:def 7;

Component_of y c= [#] (X | G) ;

then A21: R c= G by PRE_TOPC:def 5;

G c= Cl G by PRE_TOPC:18;

then A22: R c= Cl G by A21;

B <> {} X by A4;

then consider z being Point of X such that

A23: z in B by PRE_TOPC:12;

A24: B c= (Cl G) ` by A12, SUBSET_1:23;

then reconsider C = (Cl G) ` as non empty Subset of X by A23;

z in (Cl G) ` by A23, A24;

then z in [#] (X | C) by PRE_TOPC:def 5;

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

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 )

A25: Component_of z1 is a_component by CONNSP_1:40;

B c= [#] (X | ((Cl G) `)) by A24, PRE_TOPC:def 5;

then reconsider B1 = B as Subset of (X | ((Cl G) `)) ;

A26: ( Component_of z1 is connected & z1 in Component_of z1 ) by CONNSP_1:38;

B1 is connected by A16, CONNSP_1:23;

then ( B1 misses Component_of z1 or B1 c= Component_of z1 ) by A25, CONNSP_1:36;

then A27: ( B1 /\ (Component_of z1) = {} or B1 c= Component_of z1 ) by XBOOLE_0:def 7;

Component_of z1 c= [#] (X | ((Cl G) `)) ;

then S c= (Cl G) ` by PRE_TOPC:def 5;

then R /\ S c= (Cl G) /\ ((Cl G) `) by A22, XBOOLE_1:27;

then R /\ S c= {} X by A14, XBOOLE_0:def 7;

then A28: R /\ S = {} ;

V1 is_a_component_of (Cl G) ` by A25, CONNSP_1:def 6;

hence ( R is connected & S is connected & R is open & S is open & A c= R & B c= S & R misses S ) by A1, A9, A8, A18, A20, A19, A23, A27, A26, A28, Th18, CONNSP_1:23, XBOOLE_0:def 4, XBOOLE_0:def 7; :: thesis: verum

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

A1: X is locally_connected and

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

A3: A <> {} and

A4: B <> {} and

A5: A is closed and

A6: ( B is closed & 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 ) )

B = ([#] X) \ (([#] X) \ B) by PRE_TOPC:3;

then A7: ([#] X) \ B <> [#] X by A4, PRE_TOPC:4;

A <> {} X by A3;

then consider x being Point of X such that

A8: x in A by PRE_TOPC:12;

( A c= B ` & B ` is open ) by A6, SUBSET_1:23;

then consider G being Subset of X such that

A9: G is open and

A10: A c= G and

A11: Cl G c= B ` by A2, A3, A5, A7, Th20;

A12: Cl G misses B by A11, SUBSET_1:23;

A13: x in G by A10, A8;

reconsider G = G as non empty Subset of X by A3, A10;

x in [#] (X | G) by A13, PRE_TOPC:def 5;

then reconsider y = x as Point of (X | G) ;

A14: Cl G misses (Cl G) ` by XBOOLE_1:79;

assume that

A15: A is connected and

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

set H = Component_of y;

reconsider H1 = Component_of y as Subset of X by PRE_TOPC:11;

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 )

A17: Component_of y is a_component by CONNSP_1:40;

then A18: H1 is_a_component_of G by CONNSP_1:def 6;

A c= [#] (X | G) by A10, PRE_TOPC:def 5;

then reconsider A1 = A as Subset of (X | G) ;

A19: ( Component_of y is connected & y in Component_of y ) by CONNSP_1:38;

A1 is connected by A15, CONNSP_1:23;

then ( A1 misses Component_of y or A1 c= Component_of y ) by A17, CONNSP_1:36;

then A20: ( A1 /\ (Component_of y) = {} or A1 c= Component_of y ) by XBOOLE_0:def 7;

Component_of y c= [#] (X | G) ;

then A21: R c= G by PRE_TOPC:def 5;

G c= Cl G by PRE_TOPC:18;

then A22: R c= Cl G by A21;

B <> {} X by A4;

then consider z being Point of X such that

A23: z in B by PRE_TOPC:12;

A24: B c= (Cl G) ` by A12, SUBSET_1:23;

then reconsider C = (Cl G) ` as non empty Subset of X by A23;

z in (Cl G) ` by A23, A24;

then z in [#] (X | C) by PRE_TOPC:def 5;

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

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 )

A25: Component_of z1 is a_component by CONNSP_1:40;

B c= [#] (X | ((Cl G) `)) by A24, PRE_TOPC:def 5;

then reconsider B1 = B as Subset of (X | ((Cl G) `)) ;

A26: ( Component_of z1 is connected & z1 in Component_of z1 ) by CONNSP_1:38;

B1 is connected by A16, CONNSP_1:23;

then ( B1 misses Component_of z1 or B1 c= Component_of z1 ) by A25, CONNSP_1:36;

then A27: ( B1 /\ (Component_of z1) = {} or B1 c= Component_of z1 ) by XBOOLE_0:def 7;

Component_of z1 c= [#] (X | ((Cl G) `)) ;

then S c= (Cl G) ` by PRE_TOPC:def 5;

then R /\ S c= (Cl G) /\ ((Cl G) `) by A22, XBOOLE_1:27;

then R /\ S c= {} X by A14, XBOOLE_0:def 7;

then A28: R /\ S = {} ;

V1 is_a_component_of (Cl G) ` by A25, CONNSP_1:def 6;

hence ( R is connected & S is connected & R is open & S is open & A c= R & B c= S & R misses S ) by A1, A9, A8, A18, A20, A19, A23, A27, A26, A28, Th18, CONNSP_1:23, XBOOLE_0:def 4, XBOOLE_0:def 7; :: thesis: verum