submetrizable implies D. complete

Moniker1998 · Moniker1998 · commit 5603939d7012 · 2026-07-23T04:36:05.000+02:00
diff --git a/theorems/T000918.md b/theorems/T000918.md
@@ -0,0 +1,14 @@
+---
+uid: T000918
+if:
+  and:
+  - P000012: true
+  - P000112: true
+then:
+  P000221: true
+refs:
+  - zb: "1380.46022"
+    name: Rings of Continuous Functions (Gillman & Jerison)
+---
+
+See exercise 15U.3 of {{zb:1380.46022}}.
