From da6d425281534407a92ce18a22584905a7847a39 Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Tue, 8 Jul 2025 22:16:01 +0200
Subject: Update lemma name

---
 megalodon/library/cardinal.mg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'megalodon/library/cardinal.mg')

diff --git a/megalodon/library/cardinal.mg b/megalodon/library/cardinal.mg
index 4d2af41..19991b2 100644
--- a/megalodon/library/cardinal.mg
+++ b/megalodon/library/cardinal.mg
@@ -36,7 +36,7 @@ Admitted.
 Theorem subset_witness : (forall A B,(((subset A B)->(exists b,(((elem b B)/\(notelem b A))))))).
 Admitted.
 Definition family_of_subsets := fun x0 x1 : set => (forall A,(((elem A x0)->(subseteq A x1)))).
-Fact notin_emptyset : (forall a,((notelem a (emptyset)))).
+Fact emptyset : (forall a,((notelem a (emptyset)))).
 Admitted.
 Definition inhabited := fun A: set => (exists a,((elem a A))).
 Definition empty := fun x0 : set => ~((inhabited x0)).
-- 
cgit v1.2.3