let X be set ; :: thesis: ( X is ordinal implies X is ordinal-membered )
assume X is ordinal ; :: thesis: X is ordinal-membered
hence ex a being ordinal number st X c= a ; :: according to ORDINAL6:def 1 :: thesis: verum