:: deftheorem defines inf ORDINAL2:def 2 :
for X being set holds inf X = meet (On X);