proposition: Lemma not_in_compl_implies_in (A : subset ℝ) (x : ℝ) : (¬ x ∈ ℝ\A) -> (x ∈ A).
proof: Proof. Assume that (¬ x : ℝ\A). It holds that (¬ ¬ x ∈ A). We conclude that (x ∈ A). Qed.
imports: Coq.Reals.Reals Classical_Prop Automation Notations Tactics