proposition: Lemma ultra_linear_subset_union : forall a f : E, axioms a -> (forall x : E, inc x f -> is_ultra_linear_subset a x) -> is_ultra_linear_subset a (union f).
proof: Proof. ir. assert (increasing_ds_family a f). ap uls_increasing_ds. am. am. uhg; dj. ap wo_subset_increasing_union. am. am. ir. cp (H0 b H2). ufi is_ultra_linear_subset H3. ee. am. cp (union_exists H3). nin H4. ee. assert (intersection2 (union f) (punctured_downward_subset a x) = intersection2 x0 (punctured_downward_subset a x)). ap uls_union_int_rw. am. ap uls_union_downward. am. exact H0. am. am. rw H6. cp (H0 x0 H5). ufi is_ultra_linear_subset H7. ee. ap H8. am. Qed.
imports: universe