{} T in the topology of T by Th1;
then A1: {} T is open by Def2;
([#] T) \ ([#] T) = {} T by Th4;
hence [#] T is closed by A1, Def3; :: thesis: verum