proposition: Lemma uls_increasing_ds : forall a f : E, axioms a -> (forall x : E, inc x f -> is_ultra_linear_subset a x) -> increasing_ds_family a f.
proof: Proof. ir. uhg. ir. assert (sub x y \/ sub y x). apply uls_or with a; ap H0; am. nin H3. ap or_intror. ap uls_sub_downward_saturated. am. ap H0; am. ap H0; am. ap or_introl. ap uls_sub_downward_saturated. am. ap H0; am. ap H0; am. Qed.
imports: universe