proposition: Lemma uls_union_downward : forall a f z : E, axioms a -> (forall x : E, inc x f -> is_ultra_linear_subset a x) -> inc z f -> downward_saturated a (union f) z.
proof: Proof. ir. uhg. ee. am. uf sub; ir. cp (union_exists H2). nin H3; ee. cp (H0 x0 H4). uh H5. ee. uh H5; ee. uh H5; ee. ap H8; am. uf sub; ir. apply union_inc with z. am. am. ir. cp (union_exists H3). nin H5. ee. assert (sub x0 z \/ sub z x0). apply uls_or with a. ap H0; am. ap H0; am. nin H7. ap H7; am. assert (downward_saturated a x0 z). ap uls_sub_downward_saturated. am. ap H0; am. ap H0; am. ufi downward_saturated H8. ee. apply H11 with x. am. am. am. Qed.
imports: universe