let b, a be ordinal number ; :: thesis: for f being Function st f is b -limited & a in dom f holds
a in b
let f be Function; :: thesis: ( f is b -limited & a in dom f implies a in b )
assume b = sup (dom f) ; :: according to EXCHSORT:def 3 :: thesis: ( not a in dom f or a in b )
hence ( not a in dom f or a in b ) by ORDINAL2:19; :: thesis: verum