let n be set ; :: thesis: ( n is natural implies n is complex )
assume n is natural ; :: thesis: n is complex
then n in NAT by ORDINAL1:def 13;
hence n is complex ; :: thesis: verum