[STATEMENT]
lemma Follows_Bounded: "F \<in> f Fols g ==> F \<in> Always {s. f s \<le> g s}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F \<in> f Fols g \<Longrightarrow> F \<in> Always {s. f s \<le> g s}
[PROOF STEP]
by (simp add: Follows_def)