theorem :: ORDINAL2:12

for X being set holds Lim X c= On X