theorem :: ORDINAL3:71

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