theorem :: ORDINAL2:7

for X being set holds On X c= X by ORDINAL1:def 9;