proposition: Lemma setcover_inv : forall A x y:Ensemble U, covers (Ensemble U) (Power_set_PO U A) y x -> Strict_Included U x y /\ (forall z:Ensemble U, Included U x z -> Included U z y -> x = z \/ z = y).
proof: Proof. intros A x y H'; elim H'. unfold Strict_Rel_of; simpl. intros H'0 H'1; split; [ auto with sets | idtac ]. intros z H'2 H'3; try assumption. elim (classic (x = z)); auto with sets. intro H'4; right; try assumption. elim (classic (z = y)); auto with sets. intro H'5; try assumption. elim H'1. exists z; auto with sets. Qed.
imports: Ensembles Constructive_sets Relations_1 Relations_1_facts Partial_Order Cpo Powerset Powerset_facts Classical Classical_sets