theorem :: ORDINAL3:9

for A being Ordinal holds inf A = {}