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 ;
then A7: A misses ([#] X) \ C by SUBSET_1:23;
( ([#] X) \ C <> {} & C ` is closed ) by ;
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 ;
then A14: y in H ` by ;
H ` c= (([#] X) \ C) ` by ;
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 ; :: 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 ;
( A c= B ` & ([#] X) \ B is open ) by ;
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 ; :: thesis: ( A c= G & B c= H & G misses H )
(([#] X) \ B) ` c= (Cl G) ` by ;
hence ( A c= G & B c= H ) by ; :: thesis: G misses H
H c= G ` by ;
hence G misses H by SUBSET_1:23; :: thesis: verum
end;
hence X is normal ; :: thesis: verum