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 consider C being Ordinal such that
A1: ( n = ((n div^ m) *^ m) +^ C & C in m ) by ORDINAL3:def 7;
n mod^ m = n -^ ((n div^ m) *^ m) by ORDINAL3:def 8;
hence n mod^ m in m by A1, ORDINAL3:65; :: thesis: verum