proposition: Lemma leq_suborder_then : forall a b x y : E, axioms a -> sub b (U a) -> leq (suborder b a) x y -> A (inc x b) (A (inc y b) (leq a x y)).
proof: Proof. intros. ee. unfold suborder in H1. pose (leq_create_then H1). ee; am. unfold suborder in H1. pose (leq_create_then H1); ee; am. unfold suborder in H1. pose (leq_create_then H1); ee; am. Qed.
imports: universe