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

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

let y be Point of T; :: thesis:
assume y in A ; :: thesis:
then consider V, W being Subset of T such that
A6: ( V is open & W is open & x in V & y in W & V misses W ) by A1, A5, PRE_TOPC:def 10;
take V ; :: thesis:
take W ; :: thesis:
thus ( V is open & W is open & {x} c= V & y in W & V misses W ) by A6, ZFMISC_1:31; :: thesis:

end;

then consider Y, Z being Subset of T such that
A7: ( Y is open & Z is open & {x} c= Y & A c= Z & Y misses Z ) by A2, A3, Th23;
take Y ; :: thesis:
take Z ; :: thesis:
thus ( Y is open & Z is open & x in Y & A c= Z & Y misses Z ) by A7, ZFMISC_1:31; :: thesis:

end;