diff --git a/properties/P000087.md b/properties/P000087.md
index 92302e328e..6e4920b309 100644
--- a/properties/P000087.md
+++ b/properties/P000087.md
@@ -8,7 +8,9 @@ refs:
     name: Topology (Munkres)
 ---
 
-There exists a continuous group operation $(x,y)\mapsto x\cdot y$ on the space such that
+$X$ is homeomorphic to a [topological group](https://en.wikipedia.org/wiki/Topological_group).
+
+Equivalently, there exists a continuous group operation $(x,y)\mapsto x\cdot y$ on $X$ such that
 the inverse operation $x\mapsto x^{-1}$ is also continuous.
 
 Contrary to Munkres or Willard, we do not assume any separation axiom like {P3}, {P2} or {P1}.
diff --git a/properties/P000238.md b/properties/P000238.md
new file mode 100644
index 0000000000..2e03f7aa94
--- /dev/null
+++ b/properties/P000238.md
@@ -0,0 +1,24 @@
+---
+uid: P000238
+name: Has a real TVS topology
+aliases:
+  - Topological vector space
+  - TVS
+refs:
+  - wikipedia: Topological_vector_space
+    name: Topological vector space on Wikipedia
+  - zb: "0867.46001"
+    name: Functional analysis (W. Rudin, 1991)
+---
+
+$X$ is homeomorphic to a [topological vector space](https://en.wikipedia.org/wiki/Topological_vector_space) (TVS) over $\mathbb R$.
+
+Equivalently, there exists a continuous commutative group operation $(x, y) \mapsto x + y$ on $X$, and a continuous scalar multiplication operation $\mathbb{R} \times X \to X$, $(\lambda, x) \mapsto \lambda x$, where $\mathbb{R}$ has the Euclidean topology, such that these operations together satisfy the axioms of a real vector space.
+
+Some others require separation axioms like {P3} or {P2}, though we do not.
+
+----
+#### Meta-properties
+
+- This property is preserved by arbitrary products.
+- This property is preserved by $\Sigma$-products.
diff --git a/spaces/S000103/properties/P000089.md b/spaces/S000103/properties/P000089.md
index 96c90a204c..d245456cb4 100644
--- a/spaces/S000103/properties/P000089.md
+++ b/spaces/S000103/properties/P000089.md
@@ -4,7 +4,7 @@ property: P000089
 value: true
 refs:
 - zb: "0867.46001"
-  name: Functional analysis. 2nd ed. (W. Rudin, 1991)
+  name: Functional analysis (W. Rudin, 1991)
 ---
 
 $X$ is a compact convex subset of a locally convex topological vector space $\mathbb R^I$. Therefore Schauder-Tychonoff fixed point theorem (Theorem 5.28 in {{zb:0867.46001}}) applies.
diff --git a/theorems/T000877.md b/theorems/T000877.md
new file mode 100644
index 0000000000..f5004b2835
--- /dev/null
+++ b/theorems/T000877.md
@@ -0,0 +1,11 @@
+---
+uid: T000877
+if:
+  and:
+  - P000238: true
+  - P000125: true
+then:
+  P000058: false
+---
+
+A nonzero real vector space contains a $1$-dimensional subspace, which is isomorphic to $\mathbb{R}$.
diff --git a/theorems/T000878.md b/theorems/T000878.md
new file mode 100644
index 0000000000..fe209bfcef
--- /dev/null
+++ b/theorems/T000878.md
@@ -0,0 +1,9 @@
+---
+uid: T000878
+if:
+  P000238: true
+then:
+  P000087: true
+---
+
+By definition.
diff --git a/theorems/T000879.md b/theorems/T000879.md
new file mode 100644
index 0000000000..601eab743d
--- /dev/null
+++ b/theorems/T000879.md
@@ -0,0 +1,9 @@
+---
+uid: T000879
+if:
+  P000238: true
+then:
+  P000199: true
+---
+
+A straight-line homotopy deformation retracts $X$ to the origin. That is, the map $X \times [0, 1] \to X$, $(x, t) \mapsto (1-t)x$ is a null-homotopy of the identity map.
diff --git a/theorems/T000880.md b/theorems/T000880.md
new file mode 100644
index 0000000000..899656100d
--- /dev/null
+++ b/theorems/T000880.md
@@ -0,0 +1,17 @@
+---
+uid: T000880
+if:
+  P000238: true
+then:
+  P000223: true
+refs:
+  - wikipedia: Balanced_set
+    name: Balanced set on Wikipedia
+  - zb: "0867.46001"
+    name: Functional analysis. 2nd ed. (W. Rudin)
+---
+
+Every neighborhood of the origin in a topological vector space $X$
+contains a balanced open neighborhood of the origin. See {{wikipedia:Balanced_set}}
+or Theorem 1.14(a) of {{zb:0867.4600}}.
+And a balanced set is {P199}.