let n, m be natural Ordinal; :: thesis: ( {} in m & n divides m implies n c= m )
assume A1: {} in m ; :: thesis: ( not n divides m or n c= m )
given a being Ordinal such that A2: m = n *^ a ; :: according to ARYTM_3:def 3 :: thesis: n c= m
a <> {} by A1, A2, ORDINAL2:38;
hence n c= m by A2, ORDINAL3:36; :: thesis: verum