theorem Th18: :: NAGATA_1:18

for T being non empty TopSpace st ( for A being Subset of T
for U being open Subset of T st A is closed & U is open & A c= U holds
ex W being sequence of (bool the carrier of T) st
( A c= Union W & Union W c= U & ( for n being Element of NAT holds
( Cl (W . n) c= U & W . n is open ) ) ) ) holds
T is normal