proposition: Lemma mflats_setI s1 s2 : s1 \in mflats -> s2 \in mflats -> s1 :&: s2 \in mflats.
proof: Proof. rewrite !inE => s1F s2F. rewrite eqEsubset mclosure_sub andbT subsetI. rewrite -[in X in (_ \subset X) && _](eqP s1F). rewrite -[in X in _ && (_ \subset X)](eqP s2F). by rewrite !mclosure_subset ?subsetIr ?subsetIl. Qed.
imports: mathcomp(all_ssreflect)