proposition: Lemma suborder_is_suborder : forall a b : E, axioms a -> sub b (U a) -> is_suborder (suborder b a) a.
proof: Proof. ir. uf is_suborder. ee. ap suborder_axioms; am. uf suborder. am. uf suborder. rw underlying_create. am. change (mor_axioms (suborder_inclusion b a)) in |- *. ap suborder_inclusion_mor_axioms; am. Qed.
imports: universe