diff --git a/properties/P000130.md b/properties/P000130.md
index a108331cb..76d661a49 100644
--- a/properties/P000130.md
+++ b/properties/P000130.md
@@ -12,4 +12,8 @@ Given as condition (3) in {{wikipedia:Locally_compact_space}}.  See also the art
 ----
 #### Meta-properties
 
+- This property is hereditary with respect to open sets.
+- This property is hereditary with respect to closed sets.
+- This property is hereditary with respect to locally closed sets (equivalent to previous two meta-properties).
+A set $A \subseteq X$ is called [*locally closed*](https://en.wikipedia.org/wiki/Locally_closed_subset) if every $x \in A$ has neighbourhood $U$ with $U \cap A$ closed in $U$ (equivalently, $A$ is the intersection of an open set and a closed set).
 - This property is preserved by arbitrary disjoint unions.
diff --git a/properties/P000170.md b/properties/P000170.md
index f23e4aaa7..8ed05a52e 100644
--- a/properties/P000170.md
+++ b/properties/P000170.md
@@ -23,3 +23,8 @@ Equivalently, every {P16} subspace is closed in $X$ and {P130}.
 The property is defined in section 2 of {{doi:10.1007/BF02194829}}, where Theorem 2.1 shows the equivalences above.
 
 Note: this property is not to be confused with other variants of k-Hausdorff (e.g. {P171}), where k-closed is defined in terms of different notions of compactly generated space or k-space.
+
+----
+#### Meta-properties
+
+- This property is hereditary.
diff --git a/theorems/T000813.md b/theorems/T000813.md
new file mode 100644
index 000000000..443ae64cc
--- /dev/null
+++ b/theorems/T000813.md
@@ -0,0 +1,32 @@
+---
+uid: T000813
+if:
+  and:
+  - P000167: true
+  - P000051: true
+  - P000170: true
+then:
+  P000136: true
+---
+
+Let $K$ be a {P16} subset of $X$. Then
+$K$ is {P3} (since $X$ is {P170}),
+and $K$ also {P167} and {P51}.
+To show that $K$ is finite, without loss of generality we can assume that $X$ itself
+is {P16}, {P3}, {P167} and {P51}
+and show that $X$ is finite.
+
+If every point of $X$ is isolated, $X$ is finite by compactness.
+Otherwise, because $X$ is {P51}, choose $x \in X$ with Cantor–Bendixson rank $1$ (that is, $x\in X'\setminus X''$).
+So $x$ is not isolated in $X$ and there is a neighbourhood $L$ of $x$
+such that all point in $L\setminus\{x\}$ are isolated in $X$.
+Since $X$ is {P11}, we can assume $L$ is closed in $X$.
+The neighbourhood $L$ must be infinite,
+because otherwise $x$ would be isolated.
+
+Take a countably infinite set $M\subseteq L$ containing $x$.
+Since $L$ is {P203}, $M$ is closed in $L$, hence closed in $X$ and compact.
+And since $M$ is {P167} and {P16},
+it is not {P181}
+[(Explore)](https://topology.pi-base.org/spaces?q=167+%2B+16+%2B+181),
+which is a contradiction.