added lemma wfP_pfsubset

--- a/NEWS	Wed Oct 12 14:37:03 2022 +0200
+++ b/NEWS	Wed Oct 12 14:50:24 2022 +0200
@@ -30,6 +30,9 @@
       wfP_if_convertible_to_wfP
       wf_if_convertible_to_wf
 
+* Theory "HOL-Library.FSet":
+  - Added lemma wfP_pfsubset.
+
 
 New in Isabelle2022 (October 2022)
 ----------------------------------

--- 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