proposition: Lemma Inhabited_not_empty : forall X:Ensemble U, Inhabited U X -> X <> Empty_set U.
proof: Proof. intros X H'; elim H'. intros x H'0; red; intro H'1. absurd (In U X x); auto with sets. rewrite H'1; auto using Noone_in_empty with sets. Qed.
imports: Ensembles