proposition: Lemma cle_wor' E (x:= intersection E): cardinal_set E -> nonempty E -> inc x E /\ (forall y, inc y E -> x <=c y).
proof: Proof. move => sa sb. have sc:= oset_cset sa. move: (ordinal_setI sb sc) => xe; split => //. by move => y yE; split; [apply: sa | apply: sa| apply:setI_s1]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)