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