theorem :: ORDINAL3:70

for A being Ordinal holds
( {} div^ A = {} & {} mod^ A = {} & A mod^ {} = A )