proposition: Lemma wo_sub : forall a b c : E, is_wo_subset a b -> sub c b -> is_wo_subset a c.
proof: Proof. ir. uh H. ee. uhg. dj. apply linear_sub with b. am. am. apply wo_same_order with (suborder c (suborder b a)). ap suborder_trans. uh H. ee. am. am. uh H. ee. am. ap suborder_well_ordered. rw underlying_suborder. am. am. Qed.
imports: universe