proposition: Lemma uls_union_int_rw : forall a b x z : E, axioms a -> downward_saturated a b x -> inc z x -> intersection2 b (punctured_downward_subset a z) = intersection2 x (punctured_downward_subset a z).
proof: Proof. ir. ap extensionality; uf sub; ir; cp (intersection2_first H2); cp (intersection2_second H2). ap intersection2_inc. ufi downward_saturated H0; ee. apply H7 with z. am. am. ufi punctured_downward_subset H4. Ztac. ufi lt H9; ee. am. am. ap intersection2_inc. ufi downward_saturated H0; ee. ap H6; am. am. Qed.
imports: universe