let T be non empty TopSpace; :: thesis: ( T is finite & T is T_1 implies T is discrete )
assume ( T is finite & T is T_1 ) ; :: thesis: T is discrete
then for A being Subset of T holds A is closed ;
hence T is discrete by TDLAT_3:16; :: thesis: verum