let X be non empty TopSpace; ( 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
; 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; ( 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 )
; ( 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
; 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; 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; ( 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; verum