diff -r e3c289f0724b -r ae66c22ed52e src/ZF/equalities.thy
--- a/src/ZF/equalities.thy	Wed Jun 26 10:25:36 2002 +0200
+++ b/src/ZF/equalities.thy	Wed Jun 26 10:26:46 2002 +0200
@@ -126,8 +126,7 @@
      "[| a : field(r);   
          !!x. <a,x>: r ==> P;   
          !!x. <x,a>: r ==> P        |] ==> P"
-apply (unfold field_def, blast)
-done
+by (unfold field_def, blast)
 
 lemma field_subset: "field(A*B) <= A Un B"
 by blast
@@ -148,6 +147,9 @@
 lemma field_times_field: "r <= Sigma(A,B) ==> r <= field(r)*field(r)"
 by blast
 
+lemma relation_field_times_field: "relation(r) ==> r <= field(r)*field(r)"
+by (simp add: relation_def, blast) 
+
 
 (*** Image of a set under a function/relation ***)