let T be non empty discrete TopSpace; :: thesis: T is normal
let W, V be Subset of T; :: according to COMPTS_1:def 6 :: thesis: ( W = {} or V = {} or not W is closed or not V is closed or not W misses V or ex b₁, b₂ being Element of bool the carrier of T st
( b₁ is open & b₂ is open & W c= b₁ & V c= b₂ & b₁ misses b₂ ) )
assume A1: ( W <> {} & V <> {} & W is closed & V is closed & W /\ V = {} ) ; :: according to XBOOLE_0:def 7 :: thesis: ex b₁, b₂ being Element of bool the carrier of T st
( b₁ is open & b₂ is open & W c= b₁ & V c= b₂ & b₁ misses b₂ )
take P = W; :: thesis: ex b₁ being Element of bool the carrier of T st
( P is open & b₁ is open & W c= P & V c= b₁ & P misses b₁ )
take Q = V; :: thesis: ( P is open & Q is open & W c= P & V c= Q & P misses Q )
thus ( P is open & Q is open ) by TDLAT_3:17; :: thesis: ( W c= P & V c= Q & P misses Q )
thus ( W c= P & V c= Q & P /\ Q = {} ) by A1; :: according to XBOOLE_0:def 7 :: thesis: verum