--- a/src/HOL/Relation.thy Sat Mar 17 08:00:18 2012 +0100
+++ b/src/HOL/Relation.thy Sat Mar 17 11:35:18 2012 +0100
@@ -276,13 +276,17 @@
"\<forall>x\<in>S. sym (r x) \<Longrightarrow> sym (INTER S r)"
by (fast intro: symI elim: symE)
-(* FIXME thm sym_INTER [to_pred] *)
+lemma symp_INF:
+ "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (INFI S r)"
+ by (fact sym_INTER [to_pred])
lemma sym_UNION:
"\<forall>x\<in>S. sym (r x) \<Longrightarrow> sym (UNION S r)"
by (fast intro: symI elim: symE)
-(* FIXME thm sym_UNION [to_pred] *)
+lemma symp_SUP:
+ "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (SUPR S r)"
+ by (fact sym_UNION [to_pred])
subsubsection {* Antisymmetry *}