let T be TopStruct ; :: thesis: ( T is empty implies T is Hausdorff )
assume Z: T is empty ; :: thesis: T is Hausdorff
let p, q be Point of T; :: according to PRE_TOPC:def 16 :: thesis: ( p = q or ex b₁, b₂ being Element of bool the carrier of T st
( b₁ is open & b₂ is open & p in b₁ & q in b₂ & b₁ misses b₂ ) )
thus ( p = q or ex b₁, b₂ being Element of bool the carrier of T st
( b₁ is open & b₂ is open & p in b₁ & q in b₂ & b₁ misses b₂ ) ) by Z, STRUCT_0:def 10; :: thesis: verum