proposition: Lemma full_bisubset_suborder : forall a b : E, scale_bisubset a b (U a) -> is_suborder a b.
proof: Proof. ir. ap show_is_suborder. uh H; ee. uh H; ee; uh H; ee; am. uh H; ee. uh H0; ee; uh H0; ee; am. ir. assert (inc x (U a)). uh H0; ee; am. assert (inc y (U a)). uh H0; ee; am. uh H; ee. wr H6. am. am. am. Qed.
imports: Arith order