let m, n be natural Ordinal; :: thesis: ( {} in m implies n mod^ m in m )
assume {} in m ; :: thesis: n mod^ m in m
then A1: ex C being Ordinal st
( n = ((n div^ m) *^ m) +^ C & C in m ) by ORDINAL3:def 6;
n mod^ m = n -^ ((n div^ m) *^ m) by ORDINAL3:def 7;
hence n mod^ m in m by A1, ORDINAL3:52; :: thesis: verum