theorem :: ORDINAL3:10

for A being Ordinal holds inf {A} = A