theorem Th40: :: ARYTM_3:40

for a, b being natural Ordinal holds
( {} / b = {} & a / 1 = a )