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 6 :: 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 <> {} & C <> [#] X ) and
A3: A c= C and
A4: A is closed and
A5: 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;
A6: ([#] X) \ C <> {} by A2, PRE_TOPC:23;
A7: C ` is closed by A5, TOPS_1:30;
([#] X) \ C c= A ` by A3, XBOOLE_1:34;
then A misses ([#] X) \ C by SUBSET_1:43;
then consider G, H being Subset of X such that
A8: ( G is open & H is open ) and
A9: ( A c= G & ([#] X) \ C c= H ) and
A10: G misses H by A1, A2, A4, A6, A7;
take G ; :: thesis: ( G is open & A c= G & Cl G c= C )
for p being set st p in Cl G holds
p in C

proof

let p be set ; :: thesis: ( p in Cl G implies p in C )
assume A11: p in Cl G ; :: thesis: p in C
then reconsider y = p as Point of X ;
A12: H ` is closed by A8, TOPS_1:30;
G c= H ` by A10, SUBSET_1:43;
then A13: y in H ` by A11, A12, PRE_TOPC:45;
H ` c= (([#] X) \ C) ` by A9, SUBSET_1:31;
then y in (([#] X) \ C) ` by A13;
hence p in C by PRE_TOPC:22; :: thesis: verum

end;

hence ( G is open & A c= G & Cl G c= C ) by A8, A9, TARSKI:def 3; :: thesis: verum

end;

assume A14: 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
A15: ( A <> {} & B <> {} ) and
A16: ( A is closed & B is closed ) and
A17: 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:22;
then A18: ([#] X) \ B <> [#] X by A15, PRE_TOPC:23;
A19: A c= B ` by A17, SUBSET_1:43;
([#] X) \ B is open by A16, PRE_TOPC:def 6;
then consider G being Subset of X such that
A20: ( G is open & A c= G ) and
A21: Cl G c= ([#] X) \ B by A14, A15, A16, A18, A19;
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 )
Cl (Cl G) = Cl G ;
then Cl G is closed by PRE_TOPC:52;
hence ( G is open & H is open ) by A20, PRE_TOPC:def 6; :: thesis: ( A c= G & B c= H & G misses H )
(([#] X) \ B) ` c= (Cl G) ` by A21, SUBSET_1:31;
hence ( A c= G & B c= H ) by A20, PRE_TOPC:22; :: thesis: G misses H
H c= G ` by PRE_TOPC:48, XBOOLE_1:34;
hence G misses H by SUBSET_1:43; :: thesis: verum

end;

hence X is normal by COMPTS_1:def 6; :: thesis: verum