theorem :: ORDINAL2:15

for D being Ordinal
for X being set st On X <> 0 & ( for A being Ordinal st A in X holds
D c= A ) holds
D c= inf X