proposition: Lemma fset_le_in X Y : X ≤ Y ↔ ∀ x, x ∈ X → x ∈ Y.
proof: Proof. pose proof (join_sl_mor_preserving to_listset). pose proof (join_sl_mor_reflecting to_listset). setoid_rewrite <-to_listset_preserves_in. split; intros E. now apply (order_preserving (to_listset)) in E. now apply (order_reflecting (to_listset)). Qed.
imports: MathClasses.theory.lattices MathClasses.varieties.monoids MathClasses.implementations.bool MathClasses.implementations.list_finite_set MathClasses.orders.lattices MathClasses.interfaces.abstract_algebra MathClasses.interfaces.finite_sets MathClasses.interfaces.orders