src/ZF/Constructible/Rank.thy
changeset 13647 7f6f0ffc45c3
parent 13634 99a593b49b04
child 13721 2cf506c09946
     1.1 --- a/src/ZF/Constructible/Rank.thy	Mon Oct 14 10:44:32 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Rank.thy	Mon Oct 14 11:32:00 2002 +0200
     1.3 @@ -666,6 +666,12 @@
     1.4  
     1.5  
     1.6  
     1.7 +subsection {*Absoluteness of Well-Founded Relations*}
     1.8 +
     1.9 +text{*Relativized to @{term M}: Every well-founded relation is a subset of some
    1.10 +inverse image of an ordinal.  Key step is the construction (in @{term M}) of a
    1.11 +rank function.*}
    1.12 +
    1.13  locale M_wfrank = M_trancl +
    1.14    assumes wfrank_separation:
    1.15       "M(r) ==>