let T be TopSpace; :: thesis: ( T is normal iff for A, B being closed Subset of T st A misses B holds
ex U, W being open Subset of T st
( A c= U & B c= W & Cl U misses Cl W ) )

hereby :: thesis: ( ( for A, B being closed Subset of T st A misses B holds
ex U, W being open Subset of T st
( A c= U & B c= W & Cl U misses Cl W ) ) implies T is normal )

assume A1: T is normal ; :: thesis: for A1, A2 being closed Subset of T st A1 misses A2 holds
ex C1, D1 being open Subset of T st
( A1 c= C1 & A2 c= D1 & Cl C1 misses Cl D1 )
let A1, A2 be closed Subset of T; :: thesis: ( A1 misses A2 implies ex C1, D1 being open Subset of T st
( A1 c= C1 & A2 c= D1 & Cl C1 misses Cl D1 ) )
assume A1 misses A2 ; :: thesis: ex C1, D1 being open Subset of T st
( A1 c= C1 & A2 c= D1 & Cl C1 misses Cl D1 )
then consider B1, B2 being Subset of T such that
A2: B1 is open and
A3: B2 is open and
A4: A1 c= B1 and
A5: A2 c= B2 and
A6: B1 misses B2 by A1, PRE_TOPC:def 12;
A1 misses B1 ` by A4, SUBSET_1:24;
then consider C1, C2 being Subset of T such that
A7: C1 is open and
A8: C2 is open and
A9: A1 c= C1 and
A10: B1 ` c= C2 and
A11: C1 misses C2 by A1, A2, PRE_TOPC:def 12;
A12: ( Cl (C2 `) = C2 ` & C2 ` c= B1 ) by A8, A10, PRE_TOPC:22, SUBSET_1:17;
A2 misses B2 ` by A5, SUBSET_1:24;
then consider D1, D2 being Subset of T such that
A13: D1 is open and
A14: D2 is open and
A15: A2 c= D1 and
A16: B2 ` c= D2 and
A17: D1 misses D2 by A1, A3, PRE_TOPC:def 12;
reconsider C1 = C1, D1 = D1 as open Subset of T by A13, A7;
take C1 = C1; :: thesis: ex D1 being open Subset of T st
( A1 c= C1 & A2 c= D1 & Cl C1 misses Cl D1 )
take D1 = D1; :: thesis: ( A1 c= C1 & A2 c= D1 & Cl C1 misses Cl D1 )
D1 c= D2 ` by A17, SUBSET_1:23;
then A18: Cl D1 c= Cl (D2 `) by PRE_TOPC:19;
C1 c= C2 ` by A11, SUBSET_1:23;
then Cl C1 c= Cl (C2 `) by PRE_TOPC:19;
then A19: Cl C1 c= B1 by A12;
( Cl (D2 `) = D2 ` & D2 ` c= B2 ) by A14, A16, PRE_TOPC:22, SUBSET_1:17;
then Cl D1 c= B2 by A18;
hence ( A1 c= C1 & A2 c= D1 & Cl C1 misses Cl D1 ) by A6, A15, A9, A19, XBOOLE_1:64; :: thesis: verum

end;

assume A20: for A, B being closed Subset of T st A misses B holds
ex U, W being open Subset of T st
( A c= U & B c= W & Cl U misses Cl W ) ; :: thesis: T is normal
for A, B being Subset of T st A is closed & B is closed & A misses B holds
ex U, W being Subset of T st
( U is open & W is open & A c= U & B c= W & U misses W )

proof

let A, B be Subset of T; :: thesis: ( A is closed & B is closed & A misses B implies ex U, W being Subset of T st
( U is open & W is open & A c= U & B c= W & U misses W ) )
assume ( A is closed & B is closed & A misses B ) ; :: thesis: ex U, W being Subset of T st
( U is open & W is open & A c= U & B c= W & U misses W )
then consider U, W being open Subset of T such that
A21: ( A c= U & B c= W & Cl U misses Cl W ) by A20;
take U ; :: thesis: ex W being Subset of T st
( U is open & W is open & A c= U & B c= W & U misses W )
take W ; :: thesis: ( U is open & W is open & A c= U & B c= W & U misses W )
( U c= Cl U & W c= Cl W ) by PRE_TOPC:18;
hence ( U is open & W is open & A c= U & B c= W & U misses W ) by A21, XBOOLE_1:64; :: thesis: verum

end;

hence T is normal by PRE_TOPC:def 12; :: thesis: verum