let T be non empty discrete TopSpace; :: thesis: T is normal
let W, V be Subset of T; :: according to COMPTS_1:def 3 :: 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 that
W <> {} and
V <> {} and
W is closed and
V is closed and
A1: 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:15; :: 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