let T be non empty TopSpace; :: thesis:
assume that
A1: T is T_2 and
A2: T is paracompact ; :: thesis:
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 )

let A, B be Subset of T; :: thesis:
assume that
A3: A <> {} and
B <> {} and
A4: A is closed and
A5: B is closed and
A6: A misses B ; :: thesis:
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 )

let x be Point of T; :: thesis:
assume x in B ; :: thesis:
then not x in A by A6, XBOOLE_0:3;
then A7: x in A ` by SUBSET_1:29;
T is regular by A1, A2, Th24;
then consider V, W being Subset of T such that
A8: ( V is open & W is open & x in V & A c= W & V misses W ) by A3, A4, A7;
take W ; :: thesis:
take V ; :: thesis:
thus ( W is open & V is open & A c= W & x in V & W misses V ) by A8; :: thesis:

end;

then consider Y, Z being Subset of T such that
A9: ( Y is open & Z is open & A c= Y & B c= Z & Y misses Z ) by A2, A5, Th23;
take Y ; :: thesis:
take Z ; :: thesis:
thus ( Y is open & Z is open & A c= Y & B c= Z & Y misses Z ) by A9; :: thesis:

end;