author  lcp 
Fri, 23 Dec 1994 16:32:02 +0100  
changeset 831  60d850cc5fe6 
parent 814  a32b420c33d4 
child 849  013a16d3addb 
permissions  rwrr 
435  1 
(* Title: ZF/OrderType.ML 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1994 University of Cambridge 

5 

814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

6 
Order types in ZermeloFraenkel Set Theory 
435  7 
*) 
8 

9 

10 
open OrderType; 

11 

814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

12 
(*** Proofs needing the combination of Ordinal.thy and Order.thy ***) 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

13 

a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

14 
goal OrderType.thy "!!i. Ord(i) ==> well_ord(i, Memrel(i))"; 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

15 
by (rtac well_ordI 1); 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

16 
by (rtac (wf_Memrel RS wf_imp_wf_on) 1); 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

17 
by (asm_simp_tac (ZF_ss addsimps [linear_def, Memrel_iff]) 1); 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

18 
by (REPEAT (resolve_tac [ballI, Ord_linear] 1));; 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

19 
by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));; 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

20 
qed "well_ord_Memrel"; 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

21 

a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

22 
(*Kunen's Theorem 7.3 (i), page 16; see also Ordinal/Ord_in_Ord 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

23 
The smaller ordinal is an initial segment of the larger *) 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

24 
goalw OrderType.thy [pred_def, lt_def] 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

25 
"!!i j. j<i ==> j = pred(i, j, Memrel(i))"; 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

26 
by (asm_simp_tac (ZF_ss addsimps [Memrel_iff]) 1); 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

27 
by (fast_tac (eq_cs addEs [Ord_trans]) 1); 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

28 
qed "lt_eq_pred"; 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

29 

831  30 
goalw OrderType.thy [pred_def,Memrel_def] 
31 
"!!A x. x:A ==> pred(A, x, Memrel(A)) = {b:A. b:x}"; 

32 
by (fast_tac eq_cs 1); 

33 
qed "pred_Memrel"; 

34 

814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

35 
goal OrderType.thy 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

36 
"!!i. [ j<i; f: ord_iso(i,Memrel(i),j,Memrel(j)) ] ==> R"; 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

37 
by (forward_tac [lt_eq_pred] 1); 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

38 
by (etac ltE 1); 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

39 
by (rtac (well_ord_Memrel RS well_ord_iso_predE) 1 THEN 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

40 
assume_tac 3 THEN assume_tac 1); 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

41 
by (etac subst 1); 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

42 
by (asm_full_simp_tac (ZF_ss addsimps [ord_iso_def]) 1); 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

43 
(*Combining the two simplifications causes looping*) 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

44 
by (asm_simp_tac (ZF_ss addsimps [Memrel_iff]) 1); 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

45 
by (fast_tac (ZF_cs addSEs [bij_is_fun RS apply_type] addEs [Ord_trans]) 1); 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

46 
qed "Ord_iso_implies_eq_lemma"; 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

47 

a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

48 
(*Kunen's Theorem 7.3 (ii), page 16. Isomorphic ordinals are equal*) 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

49 
goal OrderType.thy 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

50 
"!!i. [ Ord(i); Ord(j); f: ord_iso(i,Memrel(i),j,Memrel(j)) \ 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

51 
\ ] ==> i=j"; 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

52 
by (res_inst_tac [("i","i"),("j","j")] Ord_linear_lt 1); 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

53 
by (REPEAT (eresolve_tac [asm_rl, ord_iso_sym, Ord_iso_implies_eq_lemma] 1)); 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

54 
qed "Ord_iso_implies_eq"; 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

55 

a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

56 
(*** Ordermap and ordertype ***) 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

57 

437  58 
goalw OrderType.thy [ordermap_def,ordertype_def] 
59 
"ordermap(A,r) : A > ordertype(A,r)"; 

60 
by (rtac lam_type 1); 

61 
by (rtac (lamI RS imageI) 1); 

62 
by (REPEAT (assume_tac 1)); 

760  63 
qed "ordermap_type"; 
437  64 

435  65 
(** Unfolding of ordermap **) 
66 

437  67 
(*Useful for cardinality reasoning; see CardinalArith.ML*) 
435  68 
goalw OrderType.thy [ordermap_def, pred_def] 
69 
"!!r. [ wf[A](r); x:A ] ==> \ 

437  70 
\ ordermap(A,r) ` x = ordermap(A,r) `` pred(A,x,r)"; 
71 
by (asm_simp_tac ZF_ss 1); 

72 
by (etac (wfrec_on RS trans) 1); 

73 
by (assume_tac 1); 

74 
by (asm_simp_tac (ZF_ss addsimps [subset_iff, image_lam, 

75 
vimage_singleton_iff]) 1); 

760  76 
qed "ordermap_eq_image"; 
437  77 

467  78 
(*Useful for rewriting PROVIDED pred is not unfolded until later!*) 
437  79 
goal OrderType.thy 
80 
"!!r. [ wf[A](r); x:A ] ==> \ 

435  81 
\ ordermap(A,r) ` x = {ordermap(A,r)`y . y : pred(A,x,r)}"; 
437  82 
by (asm_simp_tac (ZF_ss addsimps [ordermap_eq_image, pred_subset, 
83 
ordermap_type RS image_fun]) 1); 

760  84 
qed "ordermap_pred_unfold"; 
435  85 

86 
(*predunfolded version. NOT suitable for rewriting  loops!*) 

87 
val ordermap_unfold = rewrite_rule [pred_def] ordermap_pred_unfold; 

88 

89 
(** Showing that ordermap, ordertype yield ordinals **) 

90 

91 
fun ordermap_elim_tac i = 

92 
EVERY [etac (ordermap_unfold RS equalityD1 RS subsetD RS RepFunE) i, 

93 
assume_tac (i+1), 

94 
assume_tac i]; 

95 

96 
goalw OrderType.thy [well_ord_def, tot_ord_def, part_ord_def] 

97 
"!!r. [ well_ord(A,r); x:A ] ==> Ord(ordermap(A,r) ` x)"; 

98 
by (safe_tac ZF_cs); 

99 
by (wf_on_ind_tac "x" [] 1); 

100 
by (asm_simp_tac (ZF_ss addsimps [ordermap_pred_unfold]) 1); 

101 
by (rtac (Ord_is_Transset RSN (2,OrdI)) 1); 

437  102 
by (rewrite_goals_tac [pred_def,Transset_def]); 
435  103 
by (fast_tac ZF_cs 2); 
104 
by (safe_tac ZF_cs); 

105 
by (ordermap_elim_tac 1); 

106 
by (fast_tac (ZF_cs addSEs [trans_onD]) 1); 

760  107 
qed "Ord_ordermap"; 
435  108 

109 
goalw OrderType.thy [ordertype_def] 

110 
"!!r. well_ord(A,r) ==> Ord(ordertype(A,r))"; 

111 
by (rtac ([ordermap_type, subset_refl] MRS image_fun RS ssubst) 1); 

112 
by (rtac (Ord_is_Transset RSN (2,OrdI)) 1); 

113 
by (fast_tac (ZF_cs addIs [Ord_ordermap]) 2); 

437  114 
by (rewrite_goals_tac [Transset_def,well_ord_def]); 
435  115 
by (safe_tac ZF_cs); 
116 
by (ordermap_elim_tac 1); 

117 
by (fast_tac ZF_cs 1); 

760  118 
qed "Ord_ordertype"; 
435  119 

120 
(** ordermap preserves the orderings in both directions **) 

121 

122 
goal OrderType.thy 

123 
"!!r. [ <w,x>: r; wf[A](r); w: A; x: A ] ==> \ 

124 
\ ordermap(A,r)`w : ordermap(A,r)`x"; 

125 
by (eres_inst_tac [("x1", "x")] (ordermap_unfold RS ssubst) 1); 

437  126 
by (assume_tac 1); 
435  127 
by (fast_tac ZF_cs 1); 
760  128 
qed "ordermap_mono"; 
435  129 

130 
(*linearity of r is crucial here*) 

131 
goalw OrderType.thy [well_ord_def, tot_ord_def] 

132 
"!!r. [ ordermap(A,r)`w : ordermap(A,r)`x; well_ord(A,r); \ 

133 
\ w: A; x: A ] ==> <w,x>: r"; 

134 
by (safe_tac ZF_cs); 

135 
by (linear_case_tac 1); 

136 
by (fast_tac (ZF_cs addSEs [mem_not_refl RS notE]) 1); 

467  137 
by (dtac ordermap_mono 1); 
435  138 
by (REPEAT_SOME assume_tac); 
437  139 
by (etac mem_asym 1); 
140 
by (assume_tac 1); 

760  141 
qed "converse_ordermap_mono"; 
435  142 

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

143 
bind_thm ("ordermap_surj", 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
788
diff
changeset

144 
rewrite_rule [symmetric ordertype_def] 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
788
diff
changeset

145 
(ordermap_type RS surj_image)); 
435  146 

147 
goalw OrderType.thy [well_ord_def, tot_ord_def, bij_def, inj_def] 

148 
"!!r. well_ord(A,r) ==> ordermap(A,r) : bij(A, ordertype(A,r))"; 

149 
by (safe_tac ZF_cs); 

437  150 
by (rtac ordermap_type 1); 
151 
by (rtac ordermap_surj 2); 

435  152 
by (linear_case_tac 1); 
153 
(*The two cases yield similar contradictions*) 

467  154 
by (ALLGOALS (dtac ordermap_mono)); 
435  155 
by (REPEAT_SOME assume_tac); 
156 
by (ALLGOALS (asm_full_simp_tac (ZF_ss addsimps [mem_not_refl]))); 

760  157 
qed "ordermap_bij"; 
435  158 

814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

159 
(** Isomorphisms involving ordertype **) 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

160 

435  161 
goalw OrderType.thy [ord_iso_def] 
162 
"!!r. well_ord(A,r) ==> \ 

163 
\ ordermap(A,r) : ord_iso(A,r, ordertype(A,r), Memrel(ordertype(A,r)))"; 

164 
by (safe_tac ZF_cs); 

467  165 
by (rtac ordermap_bij 1); 
437  166 
by (assume_tac 1); 
467  167 
by (fast_tac (ZF_cs addSEs [MemrelE, converse_ordermap_mono]) 2); 
437  168 
by (rewtac well_ord_def); 
467  169 
by (fast_tac (ZF_cs addSIs [MemrelI, ordermap_mono, 
435  170 
ordermap_type RS apply_type]) 1); 
760  171 
qed "ordertype_ord_iso"; 
435  172 

814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

173 
goal OrderType.thy 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

174 
"!!f. [ f: ord_iso(A,r,B,s); well_ord(B,s) ] ==> \ 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

175 
\ ordertype(A,r) = ordertype(B,s)"; 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

176 
by (forward_tac [well_ord_ord_iso] 1 THEN assume_tac 1); 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

177 
by (resolve_tac [Ord_iso_implies_eq] 1 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

178 
THEN REPEAT (eresolve_tac [Ord_ordertype] 1)); 
831  179 
by (deepen_tac (ZF_cs addIs [ord_iso_trans, ord_iso_sym] 
180 
addSEs [ordertype_ord_iso]) 0 1); 

814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

181 
qed "ordertype_eq"; 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

182 

435  183 

184 
(** Unfolding of ordertype **) 

185 

186 
goalw OrderType.thy [ordertype_def] 

187 
"ordertype(A,r) = {ordermap(A,r)`y . y : A}"; 

188 
by (rtac ([ordermap_type, subset_refl] MRS image_fun) 1); 

760  189 
qed "ordertype_unfold"; 
467  190 

814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

191 
(*Ordertype of Memrel*) 
467  192 
goal OrderType.thy "!!i. Ord(i) ==> ordertype(i,Memrel(i)) = i"; 
814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

193 
by (resolve_tac [Ord_iso_implies_eq RS sym] 1); 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

194 
by (resolve_tac [ordertype_ord_iso] 3); 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

195 
by (REPEAT (ares_tac [well_ord_Memrel, Ord_ordertype] 1)); 
760  196 
qed "ordertype_Memrel"; 
467  197 

814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

198 
(*Ordertype of rvimage*) 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

199 
bind_thm ("bij_ordertype_vimage", ord_iso_rvimage RS ordertype_eq); 
467  200 

814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

201 
(*Ordermap returns the same result if applied to an initial segment*) 
467  202 
goal OrderType.thy 
203 
"!!r. [ well_ord(A,r); y:A; z: pred(A,y,r) ] ==> \ 

204 
\ ordermap(pred(A,y,r), r) ` z = ordermap(A, r) ` z"; 

205 
by (forward_tac [[well_ord_is_wf, pred_subset] MRS wf_on_subset_A] 1); 

206 
by (wf_on_ind_tac "z" [] 1); 

207 
by (safe_tac (ZF_cs addSEs [predE])); 

208 
by (asm_simp_tac 

209 
(ZF_ss addsimps [ordermap_pred_unfold, well_ord_is_wf, pred_iff]) 1); 

210 
(*combining these two simplifications LOOPS! *) 

211 
by (asm_simp_tac (ZF_ss addsimps [pred_pred_eq]) 1); 

212 
by (asm_full_simp_tac (ZF_ss addsimps [pred_def]) 1); 

807  213 
by (rtac (refl RSN (2,RepFun_cong)) 1); 
214 
by (dtac well_ord_is_trans_on 1); 

467  215 
by (fast_tac (eq_cs addSEs [trans_onD]) 1); 
760  216 
qed "ordermap_pred_eq_ordermap"; 
467  217 

814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

218 
(*Lemma for proving there exist ever larger cardinals*) 
467  219 
goal OrderType.thy 
220 
"!!r. [ well_ord(A,r); i: ordertype(A,r) ] ==> \ 

221 
\ EX B. B<=A & i = ordertype(B,r)"; 

222 
by (dresolve_tac [ordertype_unfold RS equalityD1 RS subsetD] 1); 

814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

223 
by (etac RepFunE 1); 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

224 
by (res_inst_tac [("x", "pred(A,y,r)")] exI 1); 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

225 
by (asm_simp_tac 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

226 
(ZF_ss addsimps [pred_subset, well_ord_is_wf RS ordermap_pred_unfold, 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

227 
ordertype_unfold, ordermap_pred_eq_ordermap]) 1); 
760  228 
qed "ordertype_subset"; 
467  229 