take sup X ; :: according to ORDINAL6:def 1 :: thesis: On X c= sup X
thus On X c= sup X by ORDINAL2:def 7; :: thesis: verum