proposition: Lemma same_as_suborder_is_suborder : forall a b x : E, sub x (U b) -> axioms b -> same_order a (suborder x b) -> is_suborder a b.
proof: Proof. ir. apply is_suborder_trans with (suborder x b). ufi same_order H1; ee. exact H1. ap suborder_is_suborder. exact H0. am. Qed.
imports: universe