proposition: Lemma Exercise6_31_c x: inc x inf_subsets -> inc (rep x) x.
proof: Proof. move/Zo_hi => ix. case: (emptyset_dichot x); last by move/rep_i. move => xe; case:(finite_not_infinite_set emptyset_finite); ue. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)