for T being non empty TopSpace
for A being Subset of T holds
( A is closed iff for N being convergent net of T st N is_eventually_in A holds
for x being Point of T st x in Lim N holds
x in A )