proposition: Lemma next_eq : forall a b c d x y : E, is_ultra_linear_subset a b -> is_ultra_linear_subset a c -> downward_saturated a b d -> downward_saturated a c d -> is_bottom_element a (complement b d) x -> is_bottom_element a (complement c d) y -> x = y.
proof: Proof. ir. cp (scale_next H H1 H3). cp (scale_next H0 H2 H4). ufi eq_ultra_bound H5. ufi eq_ultra_bound H6. ee. wr H8; am. Qed.
imports: universe