let n be set ; :: thesis: ( n is natural implies n is complex )
assume A1: n is natural ; :: thesis: n is complex
A2: n in NAT by A1, ORDINAL1:def 13;
thus n is complex by A2; :: thesis: verum