proposition: Lemma subset_lattice_is_complemented : LEM -> complemented_structure (make_bounded_lattice subset_lattice_is_bounded).
proof: Proof. intros lem sub. exists (subtype_complement sub). use make_dirprod. - apply (invweq (hsubtype_univalence _ _)). eapply (subtype_complement_union lem). + exists true; reflexivity. + exists false; reflexivity. - apply (invweq (hsubtype_univalence _ _)). eapply subtype_complement_intersection_empty. + exists true; reflexivity. + exists false; reflexivity. Defined.
imports: UniMath.Foundations.Preamble UniMath.Foundations.PartA UniMath.Foundations.Sets UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.OrderTheory.Lattice.Lattice UniMath.OrderTheory.Lattice.Bounded UniMath.OrderTheory.Lattice.Distributive UniMath.OrderTheory.Lattice.Complement UniMath.OrderTheory.Lattice.Boolean