From 084401a0129afe139a0125accf21b731f01bb54a Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Thu, 25 Dec 2025 19:05:40 +0100
Subject: [PATCH 1/2] implication

---
 theorems/T000808.md | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 theorems/T000808.md

diff --git a/theorems/T000808.md b/theorems/T000808.md
new file mode 100644
index 000000000..55ecd695d
--- /dev/null
+++ b/theorems/T000808.md
@@ -0,0 +1,12 @@
+---
+uid: T000808
+if:
+  P000120: true
+then:
+  P000210: true
+refs:
+  - mathse: 5116648
+    name: Do the Arkhangel'skii $\alpha_i$ properties hold for order topologies?
+---
+
+See {{mathse:5116648}}.

From 0556874e91ba39a0831bfa3f2ae76da4b8391403 Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Fri, 26 Dec 2025 13:45:05 +0100
Subject: [PATCH 2/2] add go

---
 theorems/T000809.md | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 theorems/T000809.md

diff --git a/theorems/T000809.md b/theorems/T000809.md
new file mode 100644
index 000000000..139bea2bc
--- /dev/null
+++ b/theorems/T000809.md
@@ -0,0 +1,9 @@
+---
+uid: T000809
+if:
+  P000154: true
+then:
+  P000210: true
+---
+
+By {T750} and {T808}, every {P133} is {P210}, the assertion follows as the property is hereditary.