[STATEMENT]
lemma weak_is_transitive:
 assumes "x \<in> carrier \<and> y \<in> carrier \<and> z \<in> carrier"
 shows "x \<succeq> y \<Longrightarrow> y \<succeq> z \<Longrightarrow> x \<succeq> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<succeq> y; y \<succeq> z\<rbrakk> \<Longrightarrow> x \<succeq> z
[PROOF STEP]
by (meson transD transitivity)