let k be Vertex of (canCompleteGraph n); :: thesis: k is natural
k c= n by ORDINAL1:def 2;
hence k is natural ; :: thesis: verum