:: deftheorem Def6 defines T_3 TAXONOM2:def 6 :
for Y being set
for F being Subset-Family of Y holds
( F is T_3 iff for A being Subset of Y st A in F holds
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 ) );