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