proposition: Lemma projected_bounded_sl: BoundedSemiLattice B.
proof: Proof. split. now apply (projected_com_monoid f). repeat intro; apply (injective f). now rewrite op_correct, (idempotency (&) _). Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.theory.groups