172 apply (rule allI) |
172 apply (rule allI) |
173 apply (erule_tac x = "Pow (A) -{0}" in allE) |
173 apply (erule_tac x = "Pow (A) -{0}" in allE) |
174 apply (erule impE, fast) |
174 apply (erule impE, fast) |
175 apply (elim bexE conjE exE) |
175 apply (elim bexE conjE exE) |
176 apply (rule bexI) |
176 apply (rule bexI) |
177 apply (rule conjI, assumption) |
177 apply (rule conjI, assumption) |
178 apply (rule_tac x = "LEAST i. HH (f,A,i) ={A}" in exI) |
178 apply (rule_tac x = "LEAST i. HH (f,A,i) ={A}" in exI) |
179 apply (rule_tac x = "\<lambda>j \<in> (LEAST i. HH (f,A,i) ={A}) . HH (f,A,j) " in exI) |
179 apply (rule_tac x = "\<lambda>j \<in> (LEAST i. HH (f,A,i) ={A}) . HH (f,A,j) " in exI) |
180 apply simp |
180 apply (simp_all add: ltD) |
181 apply (fast intro!: Ord_Least lam_type [THEN domain_of_fun] |
181 apply (fast intro!: Ord_Least lam_type [THEN domain_of_fun] |
182 elim!: less_Least_subset_x lemma1 lemma2, assumption) |
182 elim!: less_Least_subset_x lemma1 lemma2) |
183 done |
183 done |
184 |
184 |
185 |
185 |
186 (* ********************************************************************** *) |
186 (* ********************************************************************** *) |
187 (* The proof needed in the first case, not in the second *) |
187 (* The proof needed in the first case, not in the second *) |