[STATEMENT]
lemma tmin_le_tmax[intro, simp]: "tmin \<le> tmax"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tmin \<le> tmax
[PROOF STEP]
using nonempty_set tmin tmax
[PROOF STATE]
proof (prove)
using this:
T \<noteq> {}
?t \<in> T \<Longrightarrow> tmin \<le> ?t
tmin \<in> T
?t \<in> T \<Longrightarrow> ?t \<le> tmax
tmax \<in> T

goal (1 subgoal):
 1. tmin \<le> tmax
[PROOF STEP]
by auto