:: deftheorem defines .Result() GLIB_000:def 57 :
for F being ManySortedSet of NAT holds F .Result() = F . (F .Lifespan());