A1: ( n in 1 or 1 c= n ) by ORDINAL1:26;
( n = {} implies ( m div^ n = {} & {} *^ 1 = {} ) ) by ORDINAL2:52, ORDINAL3:def 7;
then (m div^ n) *^ 1 c= (m div^ n) *^ n by A1, ORDINAL3:17, ORDINAL3:23;
then ( m div^ n c= (m div^ n) *^ n & (m div^ n) *^ n c= m ) by ORDINAL2:56, ORDINAL3:77;
then ( m div^ n c= m & m in omega ) by ORDINAL1:def 13, XBOOLE_1:1;
hence m div^ n in omega by ORDINAL1:22; :: according to ORDINAL1:def 13 :: thesis: verum