author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 1461  6bcb44e4d6e5 
child 2469  b50b8c0eec01 
permissions  rwrr 
1461  1 
(* Title: ZF/Zorn.ML 
485  2 
ID: $Id$ 
1461  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
485  4 
Copyright 1994 University of Cambridge 
5 

516  6 
Proofs from the paper 
485  7 
Abrial & Laffitte, 
8 
Towards the Mechanization of the Proofs of Some 

9 
Classical Theorems of Set Theory. 

10 
*) 

11 

516  12 
open Zorn; 
485  13 

516  14 
(*** Section 1. Mathematical Preamble ***) 
15 

16 
goal ZF.thy "!!A B C. (ALL x:C. x<=A  B<=x) ==> Union(C)<=A  B<=Union(C)"; 

17 
by (fast_tac ZF_cs 1); 

760  18 
qed "Union_lemma0"; 
516  19 

20 
goal ZF.thy 

21 
"!!A B C. [ c:C; ALL x:C. A<=x  x<=B ] ==> A<=Inter(C)  Inter(C)<=B"; 

22 
by (fast_tac ZF_cs 1); 

760  23 
qed "Inter_lemma0"; 
516  24 

25 

26 
(*** Section 2. The Transfinite Construction ***) 

27 

28 
goalw Zorn.thy [increasing_def] 

29 
"!!f A. f: increasing(A) ==> f: Pow(A)>Pow(A)"; 

804  30 
by (etac CollectD1 1); 
760  31 
qed "increasingD1"; 
516  32 

33 
goalw Zorn.thy [increasing_def] 

34 
"!!f A. [ f: increasing(A); x<=A ] ==> x <= f`x"; 

35 
by (eresolve_tac [CollectD2 RS spec RS mp] 1); 

36 
by (assume_tac 1); 

760  37 
qed "increasingD2"; 
516  38 

485  39 
(*Introduction rules*) 
516  40 
val [TFin_nextI, Pow_TFin_UnionI] = TFin.intrs; 
485  41 
val TFin_UnionI = PowI RS Pow_TFin_UnionI; 
42 

516  43 
val TFin_is_subset = TFin.dom_subset RS subsetD RS PowD; 
485  44 

45 

46 
(** Structural induction on TFin(S,next) **) 

47 

48 
val major::prems = goal Zorn.thy 

49 
"[ n: TFin(S,next); \ 

50 
\ !!x. [ x : TFin(S,next); P(x); next: increasing(S) ] ==> P(next`x); \ 

51 
\ !!Y. [ Y <= TFin(S,next); ALL y:Y. P(y) ] ==> P(Union(Y)) \ 

52 
\ ] ==> P(n)"; 

516  53 
by (rtac (major RS TFin.induct) 1); 
485  54 
by (ALLGOALS (fast_tac (ZF_cs addIs prems))); 
760  55 
qed "TFin_induct"; 
485  56 

57 
(*Perform induction on n, then prove the major premise using prems. *) 

58 
fun TFin_ind_tac a prems i = 

59 
EVERY [res_inst_tac [("n",a)] TFin_induct i, 

1461  60 
rename_last_tac a ["1"] (i+1), 
61 
rename_last_tac a ["2"] (i+2), 

62 
ares_tac prems i]; 

485  63 

64 
(*** Section 3. Some Properties of the Transfinite Construction ***) 

65 

803
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
760
diff
changeset

66 
bind_thm ("increasing_trans", 
1461  67 
TFin_is_subset RSN (3, increasingD2 RSN (2,subset_trans))); 
485  68 

69 
(*Lemma 1 of section 3.1*) 

70 
val major::prems = goal Zorn.thy 

71 
"[ n: TFin(S,next); m: TFin(S,next); \ 

72 
\ ALL x: TFin(S,next) . x<=m > x=m  next`x<=m \ 

73 
\ ] ==> n<=m  next`m<=n"; 

74 
by (cut_facts_tac prems 1); 

804  75 
by (rtac (major RS TFin_induct) 1); 
1461  76 
by (etac Union_lemma0 2); (*or just fast_tac ZF_cs*) 
485  77 
by (fast_tac (subset_cs addIs [increasing_trans]) 1); 
760  78 
qed "TFin_linear_lemma1"; 
485  79 

80 
(*Lemma 2 of section 3.2. Interesting in its own right! 

81 
Requires next: increasing(S) in the second induction step. *) 

82 
val [major,ninc] = goal Zorn.thy 

83 
"[ m: TFin(S,next); next: increasing(S) \ 

84 
\ ] ==> ALL n: TFin(S,next) . n<=m > n=m  next`n<=m"; 

804  85 
by (rtac (major RS TFin_induct) 1); 
86 
by (rtac (impI RS ballI) 1); 

485  87 
(*case split using TFin_linear_lemma1*) 
88 
by (res_inst_tac [("n1","n"), ("m1","x")] 

89 
(TFin_linear_lemma1 RS disjE) 1 THEN REPEAT (assume_tac 1)); 

90 
by (dres_inst_tac [("x","n")] bspec 1 THEN assume_tac 1); 

91 
by (fast_tac (subset_cs addIs [increasing_trans]) 1); 

92 
by (REPEAT (ares_tac [disjI1,equalityI] 1)); 

93 
(*second induction step*) 

804  94 
by (rtac (impI RS ballI) 1); 
95 
by (rtac (Union_lemma0 RS disjE) 1); 

96 
by (etac disjI2 3); 

485  97 
by (REPEAT (ares_tac [disjI1,equalityI] 2)); 
804  98 
by (rtac ballI 1); 
485  99 
by (ball_tac 1); 
100 
by (set_mp_tac 1); 

101 
by (res_inst_tac [("n1","n"), ("m1","x")] 

102 
(TFin_linear_lemma1 RS disjE) 1 THEN REPEAT (assume_tac 1)); 

103 
by (fast_tac subset_cs 1); 

804  104 
by (rtac (ninc RS increasingD2 RS subset_trans RS disjI1) 1); 
485  105 
by (REPEAT (ares_tac [TFin_is_subset] 1)); 
760  106 
qed "TFin_linear_lemma2"; 
485  107 

108 
(*a more convenient form for Lemma 2*) 

109 
goal Zorn.thy 

110 
"!!m n. [ n<=m; m: TFin(S,next); n: TFin(S,next); next: increasing(S) \ 

111 
\ ] ==> n=m  next`n<=m"; 

804  112 
by (rtac (TFin_linear_lemma2 RS bspec RS mp) 1); 
485  113 
by (REPEAT (assume_tac 1)); 
760  114 
qed "TFin_subsetD"; 
485  115 

116 
(*Consequences from section 3.3  Property 3.2, the ordering is total*) 

117 
goal Zorn.thy 

118 
"!!m n. [ m: TFin(S,next); n: TFin(S,next); next: increasing(S) \ 

119 
\ ] ==> n<=m  m<=n"; 

804  120 
by (rtac (TFin_linear_lemma2 RSN (3,TFin_linear_lemma1) RS disjE) 1); 
485  121 
by (REPEAT (assume_tac 1) THEN etac disjI2 1); 
122 
by (fast_tac (subset_cs addIs [increasingD2 RS subset_trans, 

1461  123 
TFin_is_subset]) 1); 
760  124 
qed "TFin_subset_linear"; 
485  125 

126 

127 
(*Lemma 3 of section 3.3*) 

128 
val major::prems = goal Zorn.thy 

129 
"[ n: TFin(S,next); m: TFin(S,next); m = next`m ] ==> n<=m"; 

130 
by (cut_facts_tac prems 1); 

804  131 
by (rtac (major RS TFin_induct) 1); 
132 
by (dtac TFin_subsetD 1); 

485  133 
by (REPEAT (assume_tac 1)); 
134 
by (fast_tac (ZF_cs addEs [ssubst]) 1); 

135 
by (fast_tac (subset_cs addIs [TFin_is_subset]) 1); 

760  136 
qed "equal_next_upper"; 
485  137 

138 
(*Property 3.3 of section 3.3*) 

139 
goal Zorn.thy 

140 
"!!m. [ m: TFin(S,next); next: increasing(S) \ 

141 
\ ] ==> m = next`m <> m = Union(TFin(S,next))"; 

804  142 
by (rtac iffI 1); 
143 
by (rtac (Union_upper RS equalityI) 1); 

144 
by (rtac (equal_next_upper RS Union_least) 2); 

485  145 
by (REPEAT (assume_tac 1)); 
804  146 
by (etac ssubst 1); 
485  147 
by (rtac (increasingD2 RS equalityI) 1 THEN assume_tac 1); 
148 
by (ALLGOALS 

149 
(fast_tac (subset_cs addIs [TFin_UnionI, TFin_nextI, TFin_is_subset]))); 

760  150 
qed "equal_next_Union"; 
485  151 

152 

153 
(*** Section 4. Hausdorff's Theorem: every set contains a maximal chain ***) 

154 
(*** NB: We assume the partial ordering is <=, the subset relation! **) 

155 

156 
(** Defining the "next" operation for Hausdorff's Theorem **) 

157 

158 
goalw Zorn.thy [chain_def] "chain(A) <= Pow(A)"; 

804  159 
by (rtac Collect_subset 1); 
760  160 
qed "chain_subset_Pow"; 
485  161 

162 
goalw Zorn.thy [super_def] "super(A,c) <= chain(A)"; 

804  163 
by (rtac Collect_subset 1); 
760  164 
qed "super_subset_chain"; 
485  165 

166 
goalw Zorn.thy [maxchain_def] "maxchain(A) <= chain(A)"; 

804  167 
by (rtac Collect_subset 1); 
760  168 
qed "maxchain_subset_chain"; 
485  169 

170 
goal Zorn.thy 

1461  171 
"!!S. [ ch : (PROD X:Pow(chain(S))  {0}. X); \ 
172 
\ X : chain(S); X ~: maxchain(S) \ 

485  173 
\ ] ==> ch ` super(S,X) : super(S,X)"; 
804  174 
by (etac apply_type 1); 
485  175 
by (rewrite_goals_tac [super_def, maxchain_def]); 
176 
by (fast_tac ZF_cs 1); 

760  177 
qed "choice_super"; 
485  178 

179 
goal Zorn.thy 

1461  180 
"!!S. [ ch : (PROD X:Pow(chain(S))  {0}. X); \ 
181 
\ X : chain(S); X ~: maxchain(S) \ 

485  182 
\ ] ==> ch ` super(S,X) ~= X"; 
804  183 
by (rtac notI 1); 
184 
by (dtac choice_super 1); 

485  185 
by (assume_tac 1); 
186 
by (assume_tac 1); 

187 
by (asm_full_simp_tac (ZF_ss addsimps [super_def]) 1); 

760  188 
qed "choice_not_equals"; 
485  189 

190 
(*This justifies Definition 4.4*) 

191 
goal Zorn.thy 

1461  192 
"!!S. ch: (PROD X: Pow(chain(S)){0}. X) ==> \ 
193 
\ EX next: increasing(S). ALL X: Pow(S). \ 

485  194 
\ next`X = if(X: chain(S)maxchain(S), ch`super(S,X), X)"; 
195 
by (rtac bexI 1); 

196 
by (rtac ballI 1); 

804  197 
by (rtac beta 1); 
485  198 
by (assume_tac 1); 
804  199 
by (rewtac increasing_def); 
485  200 
by (rtac CollectI 1); 
201 
by (rtac lam_type 1); 

202 
by (asm_simp_tac (ZF_ss setloop split_tac [expand_if]) 1); 

203 
by (fast_tac (ZF_cs addSIs [super_subset_chain RS subsetD, 

1461  204 
chain_subset_Pow RS subsetD, 
205 
choice_super]) 1); 

485  206 
(*Now, verify that it increases*) 
207 
by (asm_simp_tac (ZF_ss addsimps [Pow_iff, subset_refl] 

208 
setloop split_tac [expand_if]) 1); 

209 
by (safe_tac ZF_cs); 

804  210 
by (dtac choice_super 1); 
485  211 
by (REPEAT (assume_tac 1)); 
804  212 
by (rewtac super_def); 
485  213 
by (fast_tac ZF_cs 1); 
760  214 
qed "Hausdorff_next_exists"; 
485  215 

216 
(*Lemma 4*) 

217 
goal Zorn.thy 

1461  218 
"!!S. [ c: TFin(S,next); \ 
219 
\ ch: (PROD X: Pow(chain(S)){0}. X); \ 

220 
\ next: increasing(S); \ 

221 
\ ALL X: Pow(S). next`X = \ 

222 
\ if(X: chain(S)maxchain(S), ch`super(S,X), X) \ 

485  223 
\ ] ==> c: chain(S)"; 
804  224 
by (etac TFin_induct 1); 
485  225 
by (asm_simp_tac 
226 
(ZF_ss addsimps [chain_subset_Pow RS subsetD, 

1461  227 
choice_super RS (super_subset_chain RS subsetD)] 
485  228 
setloop split_tac [expand_if]) 1); 
804  229 
by (rewtac chain_def); 
485  230 
by (rtac CollectI 1 THEN fast_tac ZF_cs 1); 
231 
(*Cannot use safe_tac: the disjunction must be left alone*) 

232 
by (REPEAT (rtac ballI 1 ORELSE etac UnionE 1)); 

233 
by (res_inst_tac [("m1","B"), ("n1","Ba")] (TFin_subset_linear RS disjE) 1); 

234 
(*fast_tac is just too slow here!*) 

235 
by (DEPTH_SOLVE (eresolve_tac [asm_rl, subsetD] 1 

236 
ORELSE ball_tac 1 THEN etac (CollectD2 RS bspec RS bspec) 1)); 

760  237 
qed "TFin_chain_lemma4"; 
485  238 

239 
goal Zorn.thy "EX c. c : maxchain(S)"; 

240 
by (rtac (AC_Pi_Pow RS exE) 1); 

241 
by (rtac (Hausdorff_next_exists RS bexE) 1); 

242 
by (assume_tac 1); 

243 
by (rename_tac "ch next" 1); 

244 
by (subgoal_tac "Union(TFin(S,next)) : chain(S)" 1); 

245 
by (REPEAT (ares_tac [TFin_chain_lemma4, subset_refl RS TFin_UnionI] 2)); 

246 
by (res_inst_tac [("x", "Union(TFin(S,next))")] exI 1); 

804  247 
by (rtac classical 1); 
485  248 
by (subgoal_tac "next ` Union(TFin(S,next)) = Union(TFin(S,next))" 1); 
249 
by (resolve_tac [equal_next_Union RS iffD2 RS sym] 2); 

250 
by (resolve_tac [subset_refl RS TFin_UnionI] 2); 

251 
by (assume_tac 2); 

804  252 
by (rtac refl 2); 
485  253 
by (asm_full_simp_tac 
254 
(ZF_ss addsimps [subset_refl RS TFin_UnionI RS 

1461  255 
(TFin.dom_subset RS subsetD)] 
485  256 
setloop split_tac [expand_if]) 1); 
257 
by (eresolve_tac [choice_not_equals RS notE] 1); 

258 
by (REPEAT (assume_tac 1)); 

760  259 
qed "Hausdorff"; 
485  260 

261 

262 
(*** Section 5. Zorn's Lemma: if all chains in S have upper bounds in S 

263 
then S contains a maximal element ***) 

264 

265 
(*Used in the proof of Zorn's Lemma*) 

266 
goalw Zorn.thy [chain_def] 

267 
"!!c. [ c: chain(A); z: A; ALL x:c. x<=z ] ==> cons(z,c) : chain(A)"; 

268 
by (fast_tac ZF_cs 1); 

760  269 
qed "chain_extend"; 
485  270 

271 
goal Zorn.thy 

272 
"!!S. ALL c: chain(S). Union(c) : S ==> EX y:S. ALL z:S. y<=z > y=z"; 

273 
by (resolve_tac [Hausdorff RS exE] 1); 

274 
by (asm_full_simp_tac (ZF_ss addsimps [maxchain_def]) 1); 

275 
by (rename_tac "c" 1); 

276 
by (res_inst_tac [("x", "Union(c)")] bexI 1); 

277 
by (fast_tac ZF_cs 2); 

278 
by (safe_tac ZF_cs); 

279 
by (rename_tac "z" 1); 

804  280 
by (rtac classical 1); 
485  281 
by (subgoal_tac "cons(z,c): super(S,c)" 1); 
282 
by (fast_tac (ZF_cs addEs [equalityE]) 1); 

804  283 
by (rewtac super_def); 
485  284 
by (safe_tac eq_cs); 
285 
by (fast_tac (ZF_cs addEs [chain_extend]) 1); 

286 
by (best_tac (ZF_cs addEs [equalityE]) 1); 

760  287 
qed "Zorn"; 
485  288 

289 

290 
(*** Section 6. Zermelo's Theorem: every set can be wellordered ***) 

291 

292 
(*Lemma 5*) 

293 
val major::prems = goal Zorn.thy 

1461  294 
"[ n: TFin(S,next); Z <= TFin(S,next); z:Z; ~ Inter(Z) : Z \ 
485  295 
\ ] ==> ALL m:Z. n<=m"; 
296 
by (cut_facts_tac prems 1); 

804  297 
by (rtac (major RS TFin_induct) 1); 
1461  298 
by (fast_tac ZF_cs 2); (*second induction step is easy*) 
804  299 
by (rtac ballI 1); 
300 
by (rtac (bspec RS TFin_subsetD RS disjE) 1); 

485  301 
by (REPEAT_SOME (eresolve_tac [asm_rl,subsetD])); 
302 
by (subgoal_tac "x = Inter(Z)" 1); 

303 
by (fast_tac ZF_cs 1); 

304 
by (fast_tac eq_cs 1); 

760  305 
qed "TFin_well_lemma5"; 
485  306 

307 
(*Wellordering of TFin(S,next)*) 

308 
goal Zorn.thy "!!Z. [ Z <= TFin(S,next); z:Z ] ==> Inter(Z) : Z"; 

804  309 
by (rtac classical 1); 
485  310 
by (subgoal_tac "Z = {Union(TFin(S,next))}" 1); 
311 
by (asm_simp_tac (ZF_ss addsimps [Inter_singleton]) 1); 

804  312 
by (etac equal_singleton 1); 
313 
by (rtac (Union_upper RS equalityI) 1); 

314 
by (rtac (subset_refl RS TFin_UnionI RS TFin_well_lemma5 RS bspec) 2); 

485  315 
by (REPEAT_SOME (eresolve_tac [asm_rl,subsetD])); 
760  316 
qed "well_ord_TFin_lemma"; 
485  317 

318 
(*This theorem just packages the previous result*) 

319 
goal Zorn.thy 

320 
"!!S. next: increasing(S) ==> \ 

321 
\ well_ord(TFin(S,next), Subset_rel(TFin(S,next)))"; 

804  322 
by (rtac well_ordI 1); 
485  323 
by (rewrite_goals_tac [Subset_rel_def, linear_def]); 
324 
(*Prove the linearity goal first*) 

325 
by (REPEAT (rtac ballI 2)); 

326 
by (excluded_middle_tac "x=y" 2); 

327 
by (fast_tac ZF_cs 3); 

328 
(*The x~=y case remains*) 

329 
by (res_inst_tac [("n1","x"), ("m1","y")] 

330 
(TFin_subset_linear RS disjE) 2 THEN REPEAT (assume_tac 2)); 

331 
by (fast_tac ZF_cs 2); 

332 
by (fast_tac ZF_cs 2); 

333 
(*Now prove the well_foundedness goal*) 

804  334 
by (rtac wf_onI 1); 
485  335 
by (forward_tac [well_ord_TFin_lemma] 1 THEN assume_tac 1); 
336 
by (dres_inst_tac [("x","Inter(Z)")] bspec 1 THEN assume_tac 1); 

337 
by (fast_tac eq_cs 1); 

760  338 
qed "well_ord_TFin"; 
485  339 

340 
(** Defining the "next" operation for Zermelo's Theorem **) 

341 

342 
goal AC.thy 

1461  343 
"!!S. [ ch : (PROD X:Pow(S)  {0}. X); X<=S; X~=S \ 
485  344 
\ ] ==> ch ` (SX) : SX"; 
804  345 
by (etac apply_type 1); 
485  346 
by (fast_tac (eq_cs addEs [equalityE]) 1); 
760  347 
qed "choice_Diff"; 
485  348 

349 
(*This justifies Definition 6.1*) 

350 
goal Zorn.thy 

1461  351 
"!!S. ch: (PROD X: Pow(S){0}. X) ==> \ 
352 
\ EX next: increasing(S). ALL X: Pow(S). \ 

485  353 
\ next`X = if(X=S, S, cons(ch`(SX), X))"; 
354 
by (rtac bexI 1); 

355 
by (rtac ballI 1); 

804  356 
by (rtac beta 1); 
485  357 
by (assume_tac 1); 
804  358 
by (rewtac increasing_def); 
485  359 
by (rtac CollectI 1); 
360 
by (rtac lam_type 1); 

361 
(*Verify that it increases*) 

804  362 
by (rtac allI 2); 
363 
by (rtac impI 2); 

485  364 
by (asm_simp_tac (ZF_ss addsimps [Pow_iff, subset_consI, subset_refl] 
365 
setloop split_tac [expand_if]) 2); 

366 
(*Type checking is surprisingly hard!*) 

367 
by (asm_simp_tac (ZF_ss addsimps [Pow_iff, cons_subset_iff, subset_refl] 

368 
setloop split_tac [expand_if]) 1); 

369 
by (fast_tac (ZF_cs addSIs [choice_Diff RS DiffD1]) 1); 

760  370 
qed "Zermelo_next_exists"; 
485  371 

372 

373 
(*The construction of the injection*) 

374 
goal Zorn.thy 

1461  375 
"!!S. [ ch: (PROD X: Pow(S){0}. X); \ 
376 
\ next: increasing(S); \ 

377 
\ ALL X: Pow(S). next`X = if(X=S, S, cons(ch`(SX), X)) \ 

378 
\ ] ==> (lam x:S. Union({y: TFin(S,next). x~: y})) \ 

485  379 
\ : inj(S, TFin(S,next)  {S})"; 
380 
by (res_inst_tac [("d", "%y. ch`(Sy)")] lam_injective 1); 

381 
by (rtac DiffI 1); 

382 
by (resolve_tac [Collect_subset RS TFin_UnionI] 1); 

383 
by (fast_tac (ZF_cs addSIs [Collect_subset RS TFin_UnionI] 

384 
addEs [equalityE]) 1); 

385 
by (subgoal_tac "x ~: Union({y: TFin(S,next). x~: y})" 1); 

386 
by (fast_tac (ZF_cs addEs [equalityE]) 2); 

387 
by (subgoal_tac "Union({y: TFin(S,next). x~: y}) ~= S" 1); 

388 
by (fast_tac (ZF_cs addEs [equalityE]) 2); 

389 
(*For proving x : next`Union(...); 

390 
Abrial & Laffitte's justification appears to be faulty.*) 

391 
by (subgoal_tac "~ next ` Union({y: TFin(S,next). x~: y}) <= \ 

392 
\ Union({y: TFin(S,next). x~: y})" 1); 

393 
by (asm_simp_tac 

394 
(ZF_ss addsimps [Collect_subset RS TFin_UnionI RS TFin_is_subset, 

1461  395 
Pow_iff, cons_subset_iff, subset_refl, 
396 
choice_Diff RS DiffD2] 

485  397 
setloop split_tac [expand_if]) 2); 
398 
by (subgoal_tac "x : next ` Union({y: TFin(S,next). x~: y})" 1); 

399 
by (fast_tac (subset_cs addSIs [Collect_subset RS TFin_UnionI, TFin_nextI]) 2); 

400 
(*End of the lemmas!*) 

401 
by (asm_full_simp_tac 

402 
(ZF_ss addsimps [Collect_subset RS TFin_UnionI RS TFin_is_subset, 

1461  403 
Pow_iff, cons_subset_iff, subset_refl] 
485  404 
setloop split_tac [expand_if]) 1); 
405 
by (REPEAT (eresolve_tac [asm_rl, consE, sym, notE] 1)); 

760  406 
qed "choice_imp_injection"; 
485  407 

408 
(*The wellordering theorem*) 

409 
goal Zorn.thy "EX r. well_ord(S,r)"; 

410 
by (rtac (AC_Pi_Pow RS exE) 1); 

411 
by (rtac (Zermelo_next_exists RS bexE) 1); 

412 
by (assume_tac 1); 

804  413 
by (rtac exI 1); 
414 
by (rtac well_ord_rvimage 1); 

415 
by (etac well_ord_TFin 2); 

485  416 
by (resolve_tac [choice_imp_injection RS inj_weaken_type] 1); 
417 
by (REPEAT (ares_tac [Diff_subset] 1)); 

760  418 
qed "AC_well_ord"; 