src/ZF/QUniv.thy
changeset 13615 449a70d88b38
parent 13357 6f54e992777e
child 16417 9bc16273c2d4
     1.1 --- a/src/ZF/QUniv.thy	Tue Oct 01 11:17:25 2002 +0200
     1.2 +++ b/src/ZF/QUniv.thy	Tue Oct 01 13:26:10 2002 +0200
     1.3 @@ -189,7 +189,7 @@
     1.4       subset_trans [OF Transset_0 [THEN QPair_Int_Vfrom_subset] QPair_mono]
     1.5  
     1.6  lemma QPair_Int_Vset_subset_UN:
     1.7 -     "Ord(i) ==> <a;b> Int Vset(i) <= (UN j:i. <a Int Vset(j); b Int Vset(j)>)"
     1.8 +     "Ord(i) ==> <a;b> Int Vset(i) <= (\<Union>j\<in>i. <a Int Vset(j); b Int Vset(j)>)"
     1.9  apply (erule Ord_cases)
    1.10  (*0 case*)
    1.11  apply (simp add: Vfrom_0)