proposition: Lemma linear_sub : forall a b c : E, is_linear_subset a b -> sub c b -> is_linear_subset a c.
proof: Proof. ir. ufi is_linear_subset H; uf is_linear_subset; dj; ee. am. uf sub; ir; au. ufi is_linear H4; uf is_linear; dj; ee. ap suborder_axioms; am. assert (inc x (U (suborder b a))). rw underlying_suborder. ap H0. rwi underlying_suborder H6. am. assert (inc y (U (suborder b a))). rw underlying_suborder. ap H0. rwi underlying_suborder H7; am. cp (H8 x y H9 H10). nin H11. ap or_introl. rwi underlying_suborder H6. rwi underlying_suborder H7. ap leq_suborder_if; try am. rwi leq_suborder_all H11; ee. am. am. am. ap or_intror. rwi underlying_suborder H6. rwi underlying_suborder H7. rw leq_suborder_all. rwi leq_suborder_all H11. xd. am. am. am. am. Qed.
imports: universe