proposition: Lemma is_suborder_leq : forall a b x y : E, is_suborder a b -> leq a x y -> leq b x y.
proof: Proof. ir. ufi is_suborder H. ee. ufi mor_axioms H3; ee. assert (b = target (inclusion a b)). uf inclusion; rw target_create. tv. rw H7. assert (x = ev (inclusion a b) x). uf inclusion; rw ev_create; tv. ufi leq H0. ee. am. assert (y = ev (inclusion a b) y). uf inclusion; rw ev_create; tv. ufi leq H0; xe. rw H8; rw H9. ap H6. uf inclusion; rw source_create; am. Qed.
imports: universe