[STATEMENT]
lemma meet_char: "a \<^bold>\<preceq> b \<longleftrightarrow> a \<^bold>\<and> b \<^bold>\<approx> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b \<^bold>\<succeq> a) = (\<forall>w. (a \<^bold>\<and> b) w = a w)
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b \<^bold>\<succeq> a) = (\<forall>w. (a w \<and> b w) = a w)
[PROOF STEP]
by blast