let n be number ; :: thesis: ( n is natural implies n is cardinal )
assume n is natural ; :: thesis: n is cardinal
then n in omega by ORDINAL1:def 12;
hence n is cardinal by Th65; :: thesis: verum