theorem :: ORDINAL2:10

for X being set holds Lim X c= X by ORDINAL1:def 10;