proposition: Lemma intersection_inc : forall x a : E, nonempty x -> (forall y : E, inc y x -> inc a y) -> inc a (intersection x).
proof: Proof. ir. unfold intersection in |- *. ap Z_inc. pose (nonempty_rep H). ap H0. am. am. Qed.
imports: tactics