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 ;
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 ;
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 ;
A13: x in G by ;
reconsider G = G as non empty Subset of X by ;
x in [#] (X | G) by ;
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 ;
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 ;
then ( A1 misses Component_of y or A1 c= Component_of y ) by ;
then A20: ( A1 /\ () = {} 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 ;
then reconsider C = (Cl G) ` as non empty Subset of X by A23;
z in (Cl G) ` by ;
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 ;
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 ;
then ( B1 misses Component_of z1 or B1 c= Component_of z1 ) by ;
then A27: ( B1 /\ () = {} 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 ;
then R /\ S c= {} X by ;
then A28: R /\ S = {} ;
V1 is_a_component_of (Cl G) ` by ;
hence ( R is connected & S is connected & R is open & S is open & A c= R & B c= S & R misses S ) by ; :: thesis: verum