let n be natural Ordinal; :: thesis: ( n divides {} & 1 divides n )
{} = n *^ {} by ORDINAL2:35;
hence n divides {} ; :: thesis: 1 divides n
n = 1 *^ n by ORDINAL2:39;
hence 1 divides n ; :: thesis: verum