proposition: Lemma suborder_axioms : forall a b : E, axioms a -> sub b (U a) -> axioms (suborder b a).
proof: Proof. intros. unfold suborder in |- *. apply create_axioms. unfold property in |- *. unfold axioms in H. ee. ir; au. ir. ap H3. exact H7. exact H8. intros. apply H4 with y; au. Qed.
imports: universe