Sequential closedness
Let
Proof
Let
be closed, , and be sequence in such that . But since is an open neighbourhood of , there exists some such that for all , so for all , a contradiction.
Main theorem
Let
Proof
The forward direction is given above. For the converse, let
such that for every sequence , implies . Suppose is not open in Then there exists some such that for every neighbourhood of , . Since is first-countable, we may construct a nested neighbourhood basis , for which for all . One may then construct a sequence such that for all . But then , contradicting the requirement that be sequentially closed. Hence must be open, whence is closed.