proposition: Lemma show_is_suborder : forall a b : E, axioms a -> axioms b -> (forall x y : E, leq a x y -> leq b x y) -> is_suborder a b.
proof: Proof. ir. uf is_suborder; ee. am. am. uf sub; ir. assert (leq b x x). ap H1. ap leq_refl; am. ufi leq H3; xe. uf inclusion. uf mor_axioms. rw source_create. rw target_create. ee. am. am. ap create_strong_axioms. uf Umorphism.property. uf Transformation.axioms. ir. assert (leq b x x). ap H1. ap leq_refl; am. ufi leq H3; xe. ir. rw ev_create. rw ev_create. ap H1; am. ufi leq H2; xe. ufi leq H2; xe. Qed.
imports: universe