let Y be set ; :: thesis: for F being Subset-Family of Y st F = {} holds
F is T_3
let F be Subset-Family of Y; :: thesis: ( F = {} implies F is T_3 )
assume A1: F = {} ; :: thesis: F is T_3
let A be Subset of Y; :: according to TAXONOM2:def 6 :: thesis: ( A in F implies for x being Element of Y st not x in A holds
ex B being Subset of Y st
( x in B & B in F & A misses B ) )
assume A2: A in F ; :: thesis: for x being Element of Y st not x in A holds
ex B being Subset of Y st
( x in B & B in F & A misses B )
let x be Element of Y; :: thesis: ( not x in A implies ex B being Subset of Y st
( x in B & B in F & A misses B ) )
assume not x in A ; :: thesis: ex B being Subset of Y st
( x in B & B in F & A misses B )
thus ex B being Subset of Y st
( x in B & B in F & A misses B ) by A1, A2; :: thesis: verum