let T be non empty TopSpace; :: thesis: ( T is T_2 & T is paracompact implies T is normal )
assume A1: ( T is T_2 & T is paracompact ) ; :: thesis: T is normal
for A, B being Subset of T st A <> {} & B <> {} & A is closed & B is closed & A misses B holds
ex W, V being Subset of T st
( W is open & V is open & A c= W & B c= V & W misses V )

proof

let A, B be Subset of T; :: thesis: ( A <> {} & B <> {} & A is closed & B is closed & A misses B implies ex W, V being Subset of T st
( W is open & V is open & A c= W & B c= V & W misses V ) )
assume that
A2: A <> {} and
B <> {} and
A3: A is closed and
A4: B is closed and
A5: A misses B ; :: thesis: ex W, V being Subset of T st
( W is open & V is open & A c= W & B c= V & W misses V )
for x being Point of T st x in B holds
ex W, V being Subset of T st
( W is open & V is open & A c= W & x in V & W misses V )

proof

let x be Point of T; :: thesis: ( x in B implies ex W, V being Subset of T st
( W is open & V is open & A c= W & x in V & W misses V ) )
assume x in B ; :: thesis: ex W, V being Subset of T st
( W is open & V is open & A c= W & x in V & W misses V )
then not x in A by A5, XBOOLE_0:3;
then A6: x in A ` by SUBSET_1:50;
T is regular by A1, Th27;
then consider V, W being Subset of T such that
A7: V is open and
A8: W is open and
A9: x in V and
A10: A c= W and
A11: V misses W by A2, A3, A6, COMPTS_1:def 5;
take W ; :: thesis: ex V being Subset of T st
( W is open & V is open & A c= W & x in V & W misses V )
take V ; :: thesis: ( W is open & V is open & A c= W & x in V & W misses V )
thus ( W is open & V is open & A c= W & x in V & W misses V ) by A7, A8, A9, A10, A11; :: thesis: verum

end;

then consider Y, Z being Subset of T such that
A12: ( Y is open & Z is open & A c= Y & B c= Z & Y misses Z ) by A1, A3, A4, A5, Th26;
take Y ; :: thesis: ex V being Subset of T st
( Y is open & V is open & A c= Y & B c= V & Y misses V )
take Z ; :: thesis: ( Y is open & Z is open & A c= Y & B c= Z & Y misses Z )
thus ( Y is open & Z is open & A c= Y & B c= Z & Y misses Z ) by A12; :: thesis: verum

end;

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