proposition: Lemma mrankE s : exists s1 : {set M}, is_rset s1 s.
proof: Proof. pose f (i : {set M}) := if i \subset s then #|i| else 0. have /eq_bigmax_cond : 0 < #|msets M|. by apply/card_gt0P; exists set0; exact: msets0. move=> /(_ f)[rs]; rewrite -big_mkcondr => rsIM rsE. have [rsSs|NrsSs] := boolP (rs \subset s). have rS : mrank s = #|rs| by rewrite /mrank rsE /f rsSs. by exists rs; split. exists set0; split; first by rewrite /mrank rsE /f (negPf NrsSs) cards0. by apply: msets0. by apply: sub0set. Qed.
imports: mathcomp(all_ssreflect)