:: deftheorem defines -limited EXCHSORT:def 3 :
for a being Ordinal
for s being set holds
( s is a -limited iff a = sup (proj1 s) );