[STATEMENT]
lemma IdeI [intro]:
    assumes "Arr T" and "set T \<subseteq> Collect R.ide"
    shows "Ide T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ide T
[PROOF STEP]
using assms Ide_char
[PROOF STATE]
proof (prove)
using this:
Arr T
set T \<subseteq> Collect R.ide
Ide ?T = (Arr ?T \<and> set ?T \<subseteq> Collect R.ide)

goal (1 subgoal):
 1. Ide T
[PROOF STEP]
by force