let X be non empty TopSpace; :: thesis: ( X is normal iff for A, C being Subset of X st A <> {} & C <> [#] X & A c= C & A is closed & C is open holds
ex G being Subset of X st
( G is open & A c= G & Cl G c= C ) )
thus ( X is normal implies for A, C being Subset of X st A <> {} & C <> [#] X & A c= C & A is closed & C is open holds
ex G being Subset of X st
( G is open & A c= G & Cl G c= C ) ) :: thesis: ( ( for A, C being Subset of X st A <> {} & C <> [#] X & A c= C & A is closed & C is open holds
ex G being Subset of X st
( G is open & A c= G & Cl G c= C ) ) implies X is normal )
proof
assume A1: for A, B being Subset of X st A <> {} & B <> {} & A is closed & B is closed & A misses B holds
ex G, H being Subset of X st
( G is open & H is open & A c= G & B c= H & G misses H ) ; :: according to COMPTS_1:def 3 :: thesis: for A, C being Subset of X st A <> {} & C <> [#] X & A c= C & A is closed & C is open holds
ex G being Subset of X st
( G is open & A c= G & Cl G c= C )
let A, C be Subset of X; :: thesis: ( A <> {} & C <> [#] X & A c= C & A is closed & C is open implies ex G being Subset of X st
( G is open & A c= G & Cl G c= C ) )
assume that
A2: A <> {} and
A3: C <> [#] X and
A4: A c= C and
A5: A is closed and
A6: C is open ; :: thesis: ex G being Subset of X st
( G is open & A c= G & Cl G c= C )
set B = ([#] X) \ C;
([#] X) \ C c= A ` by A4, XBOOLE_1:34;
then A7: A misses ([#] X) \ C by SUBSET_1:23;
( ([#] X) \ C <> {} & C ` is closed ) by A3, A6, PRE_TOPC:4;
then consider G, H being Subset of X such that
A8: G is open and
A9: H is open and
A10: A c= G and
A11: ([#] X) \ C c= H and
A12: G misses H by A1, A2, A5, A7;
take G ; :: thesis: ( G is open & A c= G & Cl G c= C )
for p being object st p in Cl G holds
p in C
proof
let p be object ; :: thesis: ( p in Cl G implies p in C )
assume A13: p in Cl G ; :: thesis: p in C
then reconsider y = p as Point of X ;
( H ` is closed & G c= H ` ) by A9, A12, SUBSET_1:23;
then A14: y in H ` by A13, PRE_TOPC:15;
H ` c= (([#] X) \ C) ` by A11, SUBSET_1:12;
then y in (([#] X) \ C) ` by A14;
hence p in C by PRE_TOPC:3; :: thesis: verum
end;
hence ( G is open & A c= G & Cl G c= C ) by A8, A10; :: thesis: verum
end;
assume A15: for A, C being Subset of X st A <> {} & C <> [#] X & A c= C & A is closed & C is open holds
ex G being Subset of X st
( G is open & A c= G & Cl G c= C ) ; :: thesis: X is normal
for A, B being Subset of X st A <> {} & B <> {} & A is closed & B is closed & A misses B holds
ex G, H being Subset of X st
( G is open & H is open & A c= G & B c= H & G misses H )
proof
let A, B be Subset of X; :: thesis: ( A <> {} & B <> {} & A is closed & B is closed & A misses B implies ex G, H being Subset of X st
( G is open & H is open & A c= G & B c= H & G misses H ) )
assume that
A16: A <> {} and
A17: B <> {} and
A18: A is closed and
A19: ( B is closed & A misses B ) ; :: thesis: ex G, H being Subset of X st
( G is open & H is open & A c= G & B c= H & G misses H )
set C = ([#] X) \ B;
([#] X) \ (([#] X) \ B) = B by PRE_TOPC:3;
then A20: ([#] X) \ B <> [#] X by A17, PRE_TOPC:4;
( A c= B ` & ([#] X) \ B is open ) by A19, PRE_TOPC:def 3, SUBSET_1:23;
then consider G being Subset of X such that
A21: G is open and
A22: A c= G and
A23: Cl G c= ([#] X) \ B by A15, A16, A18, A20;
take G ; :: thesis: ex H being Subset of X st
( G is open & H is open & A c= G & B c= H & G misses H )
take H = ([#] X) \ (Cl G); :: thesis: ( G is open & H is open & A c= G & B c= H & G misses H )
thus ( G is open & H is open ) by A21, PRE_TOPC:def 3; :: thesis: ( A c= G & B c= H & G misses H )
(([#] X) \ B) ` c= (Cl G) ` by A23, SUBSET_1:12;
hence ( A c= G & B c= H ) by A22, PRE_TOPC:3; :: thesis: G misses H
H c= G ` by PRE_TOPC:18, XBOOLE_1:34;
hence G misses H by SUBSET_1:23; :: thesis: verum
end;
hence X is normal ; :: thesis: verum