src/HOL/Library/FSet.thy

--- a/src/HOL/Library/FSet.thy	Wed Oct 12 14:37:03 2022 +0200
+++ b/src/HOL/Library/FSet.thy	Wed Oct 12 14:50:24 2022 +0200
@@ -745,6 +745,15 @@
 end
 
 
+subsubsection \<open>@{term fsubset}\<close>
+
+lemma wfP_pfsubset: "wfP (|\<subset>|)"
+proof (rule wfP_if_convertible_to_nat)
+  show "\<And>x y. x |\<subset>| y \<Longrightarrow> fcard x < fcard y"
+    by (rule pfsubset_fcard_mono)
+qed
+
+
 subsubsection \<open>Group operations\<close>
 
 locale comm_monoid_fset = comm_monoid