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